blob: 9272ed8c785fa6154004b63dcf52adf6aa172196 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* 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 = Usedepends + Divides + Primes +
consts fib :: "nat => nat"
recdef fib "less_than"
zero "fib 0 = 0"
one "fib 1 = 1"
Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)"
end
|
