aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfunemy2022-10-23 22:30:17 +0000
committerfunemy2022-10-23 22:30:17 +0000
commit72c87a2aafa2bd98952494463353b2a48c1a06f5 (patch)
treee884bec4365d870c17cbf254800e30110c5d7ec1
parente346fd18b3a830fce2e577a95854f0e7e4904070 (diff)
boring one
-rw-r--r--entries/funemy/.gitignore1
-rw-r--r--entries/funemy/agda/fib1.agda36
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
+
+