changeset 10147 | 178deaacb244 |
parent 9944 | 2a705d1af4dc |
child 11049 | 7eef34adb852 |
10146:e89309dde9d3 | 10147:178deaacb244 |
---|---|
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 = Divides + Primes + |
9 Fib = Primes + |
10 |
10 |
11 consts fib :: "nat => nat" |
11 consts fib :: "nat => nat" |
12 recdef fib "less_than" |
12 recdef fib "less_than" |
13 zero "fib 0 = 0" |
13 zero "fib 0 = 0" |
14 one "fib 1 = 1" |
14 one "fib 1 = 1" |