author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10147  178deaacb244 
child 11049  7eef34adb852 
permissions  rwrr 
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 