| author | wenzelm | 
| Fri, 03 Nov 2000 21:27:06 +0100 | |
| changeset 10379 | 93630e0c5ae9 | 
| parent 10147 | 178deaacb244 | 
| child 11049 | 7eef34adb852 | 
| permissions | -rw-r--r-- | 
| 9944 | 1 | (* Title: ex/Fib | 
| 2 | ID: $Id$ | |
| 3 | Author: Lawrence C Paulson, Cambridge University Computer Laboratory | |
| 4 | Copyright 1997 University of Cambridge | |
| 5 | ||
| 6 | The Fibonacci function. Demonstrates the use of recdef. | |
| 7 | *) | |
| 8 | ||
| 10147 | 9 | Fib = Primes + | 
| 9944 | 10 | |
| 11 | consts fib :: "nat => nat" | |
| 12 | recdef fib "less_than" | |
| 13 | zero "fib 0 = 0" | |
| 14 | one "fib 1 = 1" | |
| 15 | Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)" | |
| 16 | ||
| 17 | end |