michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/notation): adjust the implicit arguments of TransExt, and add new test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-29 17:12:50 -07:00
parent 7fc87faa8f
commit bc92671ae4
3 changed files with 25 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/notation.cpp
View file

@ -81,6 +81,7 @@ void init_builtin_notation(frontend & f) {
f.mark_implicit_arguments(mk_discharge_fn(), {true, true, false});
f.mark_implicit_arguments(mk_refl_fn(), {true, false});
f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, false, false, false});
f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, true, false, false});
f.mark_implicit_arguments(mk_eta_fn(), {true, true, false});
f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false});
f.mark_implicit_arguments(mk_dom_inj_fn(), {true, true, true, true, false});
@ -102,7 +103,6 @@ void init_builtin_notation(frontend & f) {
f.mark_implicit_arguments(mk_disj_cases_fn(), {true, true, true, false, false, false});
f.mark_implicit_arguments(mk_symm_fn(), {true, true, true, false});
f.mark_implicit_arguments(mk_trans_fn(), {true, true, true, true, false, false});
f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, false, false});
f.mark_implicit_arguments(mk_eqt_elim_fn(), {true, false});
f.mark_implicit_arguments(mk_eqt_intro_fn(), {true, false});
f.mark_implicit_arguments(mk_congr1_fn(), {true, true, true, true, false, false});

12
tests/lean/eq3.lean Normal file
View file

@ -0,0 +1,12 @@
Variable Vector : Nat -> Type
Variable n : Nat
Variable v1 : Vector n
Variable v2 : Vector (n + 0)
Variable v3 : Vector (0 + n)
Axiom H1 : v1 == v2
Axiom H2 : v2 == v3
Check TransExt H1 H2
Set pp::implicit true
Check TransExt H1 H2

12
tests/lean/eq3.lean.expected.out Normal file
View file

@ -0,0 +1,12 @@
Set: pp::colors
Set: pp::unicode
Assumed: Vector
Assumed: n
Assumed: v1
Assumed: v2
Assumed: v3
Assumed: H1
Assumed: H2
TransExt H1 H2 : v1 == v3
Set: lean::pp::implicit
TransExt::explicit (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3