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

fix(frontends/lean/util): assertion violation

Browse source 
fixes #559
This commit is contained in:
Leonardo de Moura 2015-04-24 15:08:58 -07:00
parent f723550d33
commit 6134c8822a
3 changed files with 20 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -126,9 +126,11 @@ void collect_locals(expr const & type, expr const & value, parser const & p, buf
buffer<expr> include_vars; buffer<expr> include_vars;
p.get_include_variables(include_vars); p.get_include_variables(include_vars);
for (expr const & param : include_vars) { for (expr const & param : include_vars) {
if (is_local(param)) {
collect_locals_ignoring_tactics(mlocal_type(param), ls); collect_locals_ignoring_tactics(mlocal_type(param), ls);
ls.insert(param); ls.insert(param);
} }
}
collect_locals_ignoring_tactics(type, ls); collect_locals_ignoring_tactics(type, ls);
collect_locals_ignoring_tactics(value, ls); collect_locals_ignoring_tactics(value, ls);
sort_locals(ls, p, ctx_ps); sort_locals(ls, p, ctx_ps);

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

@ -0,0 +1,12 @@
import algebra.ordered_field
open algebra
section sequence_c
parameter Q : Type
parameter lof_Q : linear_ordered_field Q
definition to_lof [instance] : linear_ordered_field Q := lof_Q
include to_lof
theorem foo (a b : Q) : a + b = b + a := !add.comm
end sequence_c

4
tests/lean/559.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
559.lean:10:28: error: failed to synthesize placeholder
Q : Type,
a b : Q
⊢ has_add Q