an agda file that is kinda like how datatypes would be encoded in quox
This commit is contained in:
parent
f7571ce6c3
commit
8f860cc1be
1 changed files with 44 additions and 0 deletions
44
quox-nat.agda
Normal file
44
quox-nat.agda
Normal file
|
@ -0,0 +1,44 @@
|
||||||
|
open import Axiom.Extensionality.Propositional
|
||||||
|
|
||||||
|
module _ (ext : ∀ {a b} → Extensionality a b) where
|
||||||
|
|
||||||
|
open import Prelude hiding (zero; suc)
|
||||||
|
open import Data.W
|
||||||
|
open import Data.Container
|
||||||
|
open import Data.Container.Relation.Unary.All ; open □
|
||||||
|
|
||||||
|
variable ℓ : Level
|
||||||
|
|
||||||
|
|
||||||
|
data Tag : Set where `zero `suc : Tag
|
||||||
|
|
||||||
|
Body : Tag → Set
|
||||||
|
Body t = case t of λ {`zero → ⊥ ; `suc → ⊤}
|
||||||
|
|
||||||
|
Repr : Container lzero lzero
|
||||||
|
Repr = Tag ▷ Body
|
||||||
|
|
||||||
|
Nat : Set
|
||||||
|
Nat = W Repr
|
||||||
|
|
||||||
|
Nat′ : Set
|
||||||
|
Nat′ = ⟦ Repr ⟧ Nat
|
||||||
|
|
||||||
|
zero : Nat
|
||||||
|
zero = sup (`zero , λ ())
|
||||||
|
|
||||||
|
suc : Nat → Nat
|
||||||
|
suc n = sup (`suc , const n)
|
||||||
|
|
||||||
|
elim : (P : Nat → Set ℓ) →
|
||||||
|
(Z : P zero) →
|
||||||
|
(S : ∀ n → P n → P (suc n)) →
|
||||||
|
(n : Nat) → P n
|
||||||
|
elim P Z S = induction P λ {(tag , body)} →
|
||||||
|
(case tag
|
||||||
|
return (λ t → (n′ : Body t → Nat) →
|
||||||
|
□ Repr P (t , n′) →
|
||||||
|
P (sup (t , n′)))
|
||||||
|
of λ where
|
||||||
|
`zero → λ n′ _ → ≡.subst (λ n′ → P (sup (`zero , n′))) (ext λ ()) Z
|
||||||
|
`suc → λ n′ IH → S (n′ tt) (IH .proof tt)) body
|
Loading…
Reference in a new issue