Commit f255878e authored by Raphael Cauderlier's avatar Raphael Cauderlier

Add some type annotation on lambdas to help dedukti type check the generated terms

parent 123da7fa
......@@ -258,10 +258,10 @@ def or_intro_2 (a : prop) (b : prop) (Hb : proof b) : proof (or a b) :=
def or_elim (a : prop) (b : prop) (c : prop) (H : proof (or a b)) (fa : proof a -> proof c) (fb : proof b -> proof c) : proof c :=
H c fa fb.
def imp_intro (a : prop) (b : prop) (f : proof a -> proof b) : proof (imp a b) := f.
thm imp_intro (a : prop) (b : prop) (f : proof a -> proof b) : proof (imp a b) := f.
def imp_elim (a : prop) (b : prop) (H : proof (imp a b)) : proof a -> proof b := H.
def all_intro (A : sort) (p : term A -> prop)
thm all_intro (A : sort) (p : term A -> prop)
(f : a : term A -> proof (p a)) : proof (all A p) := f.
def all_elim (A : sort) (p : term A -> prop)
(H : proof (all A p)) : a : term A -> proof (p a) := H.
......
......@@ -51,13 +51,13 @@ def mintro_proof : A : prop ->
[A,B,b] mintro_term A B (x => mret (B x) (b x))
-->
mret (all A B) (fol.all_intro A B (x => b x))
mret (all A B) (fol.all_intro A B (x : term A => b x))
[A,B,e] mintro_term A B (x => mraise (B x) e)
-->
mraise (all A B) e.
[A,B,b] mintro_proof A B (x => mret B (b x))
-->
mret (imp A B) (fol.imp_intro A B (x => b x))
mret (imp A B) (fol.imp_intro A B (x : proof A => b x))
[A,B,e] mintro_proof A B (x => mraise _ e)
-->
mraise (imp A B) e.
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