| changeset 1150 | 66512c9e6bd6 |
| parent 244 | 929fc2c63bd0 |
| child 1168 | 74be52691d62 |
| 1149:5750eba8820d | 1150:66512c9e6bd6 |
|---|---|
14 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
14 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
15 |
15 |
16 rules |
16 rules |
17 |
17 |
18 step_def "step == (LAM b g x. If b[x] then g[x] else x fi)" |
18 step_def "step == (LAM b g x. If b[x] then g[x] else x fi)" |
19 while_def "while == (LAM b g. fix[LAM f x.\ |
19 while_def "while == (LAM b g. fix[LAM f x. |
20 \ If b[x] then f[g[x]] else x fi])" |
20 If b[x] then f[g[x]] else x fi])" |
21 |
21 |
22 |
22 |
23 end |
23 end |
24 |
24 |