Skip to content

Instantly share code, notes, and snippets.

@MaiaVictor MaiaVictor/ind-self-ex.agda Secret
Created Sep 27, 2018

Embed
What would you like to do?
induction with self-referring types
Nat : (n : Nat n) -> Set
Nat =
λ (n : Nat n)
(P : (n : Nat n) -> Set)
(S : (n : Nat n) -> P n -> P (Succ n))
(Z : P Zero)
P n
Zero : Nat Zero
Zero =
λ (P : (n : Nat n) -> Set)
λ (S : (n : Nat n) -> P n -> P (Succ n))
λ (Z : P Zero)
Z
Succ : (n : Nat n) -> Nat (Succ n)
Succ =
λ (n : Nat n)
λ (P : (n : Nat n) -> Set)
λ (S : (n : Nat n) -> P n -> P (Succ n))
λ (Z : P Zero)
S n (n P S Z)
ind :
(P : (n : Nat n) -> Set)
(S : (n : Nat n) -> P n -> P (Succ n))
(Z : P Zero)
(n : Nat n)
P n
ind =
λ (P : (n : Nat n) -> Set)
λ (S : (n : Nat n) -> P n -> P (Succ n))
λ (Z : P Zero)
λ (n : Nat n)
n P S Z
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.