src/HOL/NumberTheory/Fib.thy
author wenzelm
Tue Oct 03 22:37:16 2000 +0200 (2000-10-03)
changeset 10147 178deaacb244
parent 9944 2a705d1af4dc
child 11049 7eef34adb852
permissions -rw-r--r--
tuned deps;
     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 
     9 Fib = Primes +
    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