equal
deleted
inserted
replaced
8 theory Dnat imports HOLCF begin |
8 theory Dnat imports HOLCF begin |
9 |
9 |
10 domain dnat = dzero | dsucc (dpred :: dnat) |
10 domain dnat = dzero | dsucc (dpred :: dnat) |
11 |
11 |
12 definition |
12 definition |
13 iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" |
13 iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where |
14 "iterator = fix $ (LAM h n f x. |
14 "iterator = fix $ (LAM h n f x. |
15 case n of dzero => x |
15 case n of dzero => x |
16 | dsucc $ m => f $ (h $ m $ f $ x))" |
16 | dsucc $ m => f $ (h $ m $ f $ x))" |
17 |
17 |
18 text {* |
18 text {* |