Make Jon's work/description consistent with everyone else

1 files changed, 0 insertions, 19 deletions

diff --git a/entries/ionchy/agda/Fib.agda b/entries/ionchy/agda/Fib.agda
deleted file mode 100644
index a12b0a5..0000000
--- a/entries/ionchy/agda/Fib.agda
+++ /dev/null
@@ -1,19 +0,0 @@
-
-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]`. -}