equal
deleted
inserted
replaced
12 consts |
12 consts |
13 |
13 |
14 iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" |
14 iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" |
15 |
15 |
16 |
16 |
17 rules |
17 defs |
18 |
18 |
19 iterator_def "iterator = fix[LAM h n f x. |
19 iterator_def "iterator == fix`(LAM h n f x. |
20 dnat_when[x][LAM m.f[h[m][f][x]]][n]]" |
20 dnat_when `x `(LAM m.f`(h`m`f`x)) `n)" |
21 |
|
22 |
|
23 end |
21 end |
24 |
|
25 |
22 |
26 (* |
23 (* |
27 |
24 |
28 iterator[UU][f][x] = UU |
25 iterator`UU`f`x = UU |
29 iterator[dzero][f][x] = x |
26 iterator`dzero`f`x = x |
30 n~=UU --> iterator[dsucc[n]][f][x] = f[iterator[n][f][x]] |
27 n~=UU --> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x) |
31 *) |
28 *) |
32 |
29 |