Commit 651022fb authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Adding an example reflexivityRoot coming from Agda

parent c704bf4c
#NAME ReflexivityRoot.
nat : Type.
0 : nat.
S : nat -> nat.
def plus : nat -> nat -> nat.
[n] plus 0 n --> n
[m,n] plus (S m) n --> S (plus m n).
def mult : nat -> nat -> nat.
[] mult 0 _ --> 0
[m,n] mult (S m) n --> plus n (mult m n).
square : nat -> Type.
sq : n : nat -> square (mult n n).
def root : n : nat -> square n -> nat.
[n] root _ (sq n) --> n.
eq : nat -> nat -> Type.
refl : n : nat -> eq n n.
def root_correct (n : nat) : eq (root (mult n n) (sq n)) n
:= refl n.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment