| changeset 6481 | dbf2d9b3d6c8 |
| parent 4809 | 595f905cc348 |
| child 8658 | 3cf533397c5a |
| 6480:c58bc3d2ba0f | 6481:dbf2d9b3d6c8 |
|---|---|
4 Copyright 1997 University of Cambridge |
4 Copyright 1997 University of Cambridge |
5 |
5 |
6 The Fibonacci function. Demonstrates the use of recdef. |
6 The Fibonacci function. Demonstrates the use of recdef. |
7 *) |
7 *) |
8 |
8 |
9 Fib = WF_Rel + Divides + Primes + |
9 Fib = Divides + Primes + |
10 |
10 |
11 consts fib :: "nat => nat" |
11 consts fib :: "nat => nat" |
12 recdef fib "less_than" |
12 recdef fib "less_than" |
13 "fib 0 = 0" |
13 "fib 0 = 0" |
14 "fib 1 = 1" |
14 "fib 1 = 1" |