blob: a12b0a5870947eff85bdd4b2326f0ff95301c3a8 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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]`. -}
|
