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@3300: Fibonacci numbers and other simple examples of recursive definitions
paulson@3300: 	(the TFL package)
paulson@3300: *)
paulson@3300: 
paulson@3300: Fib = WF_Rel +
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