diff options
| author | funemy | 2022-10-23 22:30:17 +0000 |
|---|---|---|
| committer | funemy | 2022-10-23 22:30:17 +0000 |
| commit | 72c87a2aafa2bd98952494463353b2a48c1a06f5 (patch) | |
| tree | e884bec4365d870c17cbf254800e30110c5d7ec1 | |
| parent | e346fd18b3a830fce2e577a95854f0e7e4904070 (diff) | |
boring one
| -rw-r--r-- | entries/funemy/.gitignore | 1 | ||||
| -rw-r--r-- | entries/funemy/agda/fib1.agda | 36 |
2 files changed, 37 insertions, 0 deletions
diff --git a/entries/funemy/.gitignore b/entries/funemy/.gitignore new file mode 100644 index 0000000..171a389 --- /dev/null +++ b/entries/funemy/.gitignore @@ -0,0 +1 @@ +*.agdai diff --git a/entries/funemy/agda/fib1.agda b/entries/funemy/agda/fib1.agda new file mode 100644 index 0000000..9e7f82a --- /dev/null +++ b/entries/funemy/agda/fib1.agda @@ -0,0 +1,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 + + |