Skip to content

Instantly share code, notes, and snippets.

@bishboria

bishboria/SingleCaseInduction.agda

Created March 23, 2014 10:49
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save bishboria/9721521 to your computer and use it in GitHub Desktop.
Save bishboria/9721521 to your computer and use it in GitHub Desktop.
Download ZIP
Single case induction
Raw
SingleCaseInduction.agda
module SingleCaseInduction where
-- Usual definition of ℕ
data N : Set where
z : N
s : N → N
-- Single case definition of ℕ
data _+_ (A : Set) (B : Set) : Set where
inl : A → A + B
inr : B → A + B
record ⊤ : Set where
data ℕ : Set where
s : (⊤ + ℕ) → ℕ
-- Usage…
z₁ : N
z₁ = z
1₁ : N
1₁ = s z
2₁ : N
2₁ = s (s z)
z₂ : ℕ
z₂ = s (inl _)
1₂ : ℕ
1₂ = s (inr (s (inl _)))
2₂ : ℕ
2₂ = s (inr (s (inr (s (inl _)))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment