| changeset 4905 | be73ddff6c5a |
| child 17248 | 81bf91654e73 |
| 4904:5f6b2dd1cd11 | 4905:be73ddff6c5a |
|---|---|
1 |
|
2 (*** Example 3.8 ***) |
|
3 |
|
4 Ex2 = LCF + |
|
5 |
|
6 consts |
|
7 P :: "'a => tr" |
|
8 F :: "'a => 'a" |
|
9 G :: "'a => 'a" |
|
10 H :: "'a => 'b => 'b" |
|
11 K :: "('a => 'b => 'b) => ('a => 'b => 'b)" |
|
12 |
|
13 rules |
|
14 F_strict "F(UU) = UU" |
|
15 K "K = (%h x y. P(x) => y | F(h(G(x),y)))" |
|
16 H "H = FIX(K)" |
|
17 |
|
18 end |