equal
deleted
inserted
replaced
8 theory Loop |
8 theory Loop |
9 imports HOLCF |
9 imports HOLCF |
10 begin |
10 begin |
11 |
11 |
12 definition |
12 definition |
13 step :: "('a -> tr)->('a -> 'a)->'a->'a" |
13 step :: "('a -> tr)->('a -> 'a)->'a->'a" where |
14 "step = (LAM b g x. If b$x then g$x else x fi)" |
14 "step = (LAM b g x. If b$x then g$x else x fi)" |
15 |
15 |
16 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
16 definition |
|
17 while :: "('a -> tr)->('a -> 'a)->'a->'a" where |
17 "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))" |
18 "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))" |
18 |
19 |
19 (* ------------------------------------------------------------------------- *) |
20 (* ------------------------------------------------------------------------- *) |
20 (* access to definitions *) |
21 (* access to definitions *) |
21 (* ------------------------------------------------------------------------- *) |
22 (* ------------------------------------------------------------------------- *) |