changeset 4809 | 595f905cc348 |
parent 3494 | f7ac2d1e2051 |
child 6481 | dbf2d9b3d6c8 |
4808:995bc5bd8319 | 4809:595f905cc348 |
---|---|
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 + |
9 Fib = WF_Rel + 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" |