From 760fb3275b2af023d099a8c1e2a143cab41c5c6b Mon Sep 17 00:00:00 2001
From: Jonathan Chan
Date: Sun, 23 Oct 2022 16:17:39 -0700
Subject: Create Fib.agda

---
 entries/ionchy/agda/Fib.agda | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 entries/ionchy/agda/Fib.agda

diff --git a/entries/ionchy/agda/Fib.agda b/entries/ionchy/agda/Fib.agda
new file mode 100644
index 0000000..a12b0a5
--- /dev/null
+++ b/entries/ionchy/agda/Fib.agda
@@ -0,0 +1,19 @@
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.List
+open import Agda.Builtin.Reflection
+
+data Fib : Nat → Nat → Set where
+  instance F0 : Fib 0 0
+  instance F1 : Fib 1 1
+  instance Fk : ∀ {k n m} → ⦃ Fib k n ⦄ → ⦃ Fib (suc k) m ⦄ → Fib (suc (suc k)) (n + m)
+
+fib' : ∀ k {n} → ⦃ Fib k n ⦄ → Nat
+fib' k {n} ⦃ fib ⦄ = n
+
+macro
+  fib : Term → Term → TC _
+  fib t hole = unify hole (def (quote fib') (arg i t ∷ []))
+    where i = arg-info visible (modality relevant quantity-ω)
+
+{- Get the [n]th Fibonacci number by normalization via C-n `fib [n]`. -}
-- 
cgit v1.2.3-70-g09d2