paulson@3300: (*  Title:      ex/Fib
paulson@3300:     ID:         $Id$
paulson@3300:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3300:     Copyright   1997  University of Cambridge
paulson@3300: 
paulson@3494: The Fibonacci function.  Demonstrates the use of recdef.
paulson@3300: *)
paulson@3300: 
paulson@3375: Fib = WF_Rel + Divides +
paulson@3300: 
paulson@3300: consts fib  :: "nat => nat"
paulson@3300: recdef fib "less_than"
paulson@3300:     "fib 0 = 0"
paulson@3300:     "fib 1 = 1"
paulson@3300:     "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
paulson@3300: 
paulson@3300: end