| changeset 3375 | d9b30c300f1e |
| parent 3300 | 4f5ffefa7799 |
| child 3494 | f7ac2d1e2051 |
| 3374:182a2b76d19e | 3375:d9b30c300f1e |
|---|---|
5 |
5 |
6 Fibonacci numbers and other simple examples of recursive definitions |
6 Fibonacci numbers and other simple examples of recursive definitions |
7 (the TFL package) |
7 (the TFL package) |
8 *) |
8 *) |
9 |
9 |
10 Fib = WF_Rel + |
10 Fib = WF_Rel + Divides + |
11 |
11 |
12 consts fib :: "nat => nat" |
12 consts fib :: "nat => nat" |
13 recdef fib "less_than" |
13 recdef fib "less_than" |
14 "fib 0 = 0" |
14 "fib 0 = 0" |
15 "fib 1 = 1" |
15 "fib 1 = 1" |