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

fix(frontends/lean/decl_cmds): assertion violation

Browse source 
closes #506
This commit is contained in:
Leonardo de Moura 2015-03-25 13:42:07 -07:00
parent d39478a028
commit 5f1d827b26
3 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -510,7 +510,7 @@ static void validate_equation_lhs(parser const & p, expr const & lhs, buffer<exp
std::any_of(locals.begin(), locals.end(), [&](expr const & local) { std::any_of(locals.begin(), locals.end(), [&](expr const & local) {
return mlocal_name(e) == mlocal_name(local); return mlocal_name(e) == mlocal_name(local);
})) { })) {
throw parser_error(sstream() << "invalid occurrence of variable '" << mlocal_name(lhs) << throw parser_error(sstream() << "invalid occurrence of variable '" << mlocal_name(e) <<
"' in the left-hand-side of recursive equation", p.pos_of(lhs)); "' in the left-hand-side of recursive equation", p.pos_of(lhs));
} }
return has_local(e); return has_local(e);

3
tests/lean/match_bug.lean Normal file
View file

@ -0,0 +1,3 @@
definition foo : nat -> nat := fun x,
match x with
| bar -> bar

1
tests/lean/match_bug.lean.expected.out Normal file
View file

@ -0,0 +1 @@
match_bug.lean:3:6: error: invalid occurrence of variable 'bar' in the left-hand-side of recursive equation