max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/decl_util): double-elaboration of include params

Browse source
This commit is contained in:
Sebastian Ullrich 2017-05-11 14:31:37 +02:00 • committed by Leonardo de Moura
parent 818c041922
commit 14425bd2d3
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -273,8 +273,6 @@ void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> &
for (expr const & e : all_exprs) {
collect_locals_ignoring_tactics(e, locals);
lp_found = collect_univ_params_ignoring_tactics(e, lp_found);
if (is_local(e))
given_params.insert(mlocal_name(e));
}
collect_annonymous_inst_implicit(p, locals);
sort_locals(locals.get_collected(), p, params);

5
tests/lean/run/include_bug.lean Normal file
View file

@ -0,0 +1,5 @@
variables x y : nat
variable xy : x = y
include xy
lemma xyeq : x = y := xy