equal
deleted
inserted
replaced
1 (* Title: ex/Fib |
1 (* Title: ex/Fib |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1997 University of Cambridge |
4 Copyright 1997 University of Cambridge |
5 |
5 |
6 Fibonacci numbers and other simple examples of recursive definitions |
6 The Fibonacci function. Demonstrates the use of recdef. |
7 (the TFL package) |
|
8 *) |
7 *) |
9 |
8 |
10 Fib = WF_Rel + Divides + |
9 Fib = WF_Rel + Divides + |
11 |
10 |
12 consts fib :: "nat => nat" |
11 consts fib :: "nat => nat" |