blob: 9e7f82adba151e25557fd7dcb8f31bee48837030 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
open import Agda.Builtin.Equality
data Nat : Set where
zero : Nat
suc : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}
z : Nat
z = zero
one : Nat
one = suc zero
add : Nat → Nat → Nat
add zero y = y
add (suc x) y = suc (add x y)
fib : Nat → Nat
fib zero = zero
fib (suc zero) = suc zero
fib (suc (suc x)) = add (fib x) (fib (suc x))
fib0 : fib 0 ≡ 0
fib0 = refl
fib1 : fib 1 ≡ 1
fib1 = refl
fib2 : fib 2 ≡ 1
fib2 = refl
fib8 : fib 8 ≡ 21
fib8 = refl
|
