| changeset 1150 | 66512c9e6bd6 |
| parent 243 | c22b85994e17 |
| child 1168 | 74be52691d62 |
| 1149:5750eba8820d | 1150:66512c9e6bd6 |
|---|---|
14 iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" |
14 iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" |
15 |
15 |
16 |
16 |
17 rules |
17 rules |
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 |
21 |
22 |
22 |
23 end |
23 end |
24 |
24 |
25 |
25 |