diff options
author | Jonathan Chan | 2022-10-23 23:17:39 +0000 |
---|---|---|
committer | GitHub | 2022-10-23 23:17:39 +0000 |
commit | 760fb3275b2af023d099a8c1e2a143cab41c5c6b (patch) | |
tree | 37bc0ab184df66e57396debb1b4dfda0a963a3be /entries | |
parent | a7d8da6952af7f5f5e33fb8c54e9a0ffb15de47b (diff) |
Create Fib.agda
Diffstat (limited to 'entries')
-rw-r--r-- | entries/ionchy/agda/Fib.agda | 19 |
1 files changed, 19 insertions, 0 deletions
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]`. -} |