author | wenzelm |
Mon, 16 Nov 1998 10:41:08 +0100 | |
changeset 5869 | b279a84ac11c |
parent 4809 | 595f905cc348 |
child 6481 | dbf2d9b3d6c8 |
permissions | -rw-r--r-- |
(* Title: ex/Fib ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge The Fibonacci function. Demonstrates the use of recdef. *) Fib = WF_Rel + Divides + Primes + consts fib :: "nat => nat" recdef fib "less_than" "fib 0 = 0" "fib 1 = 1" "fib (Suc(Suc x)) = (fib x + fib (Suc x))" end