changeset 8658 | 3cf533397c5a |
parent 6481 | dbf2d9b3d6c8 |
8657:b9475dad85ed | 8658:3cf533397c5a |
---|---|
8 |
8 |
9 Fib = Divides + Primes + |
9 Fib = Divides + Primes + |
10 |
10 |
11 consts fib :: "nat => nat" |
11 consts fib :: "nat => nat" |
12 recdef fib "less_than" |
12 recdef fib "less_than" |
13 "fib 0 = 0" |
13 zero "fib 0 = 0" |
14 "fib 1 = 1" |
14 one "fib 1 = 1" |
15 "fib (Suc(Suc x)) = (fib x + fib (Suc x))" |
15 Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
16 |
16 |
17 end |
17 end |