diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 901be56a2..b1128e936 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -510,7 +510,7 @@ static void validate_equation_lhs(parser const & p, expr const & lhs, buffer nat := fun x, +match x with +| bar -> bar diff --git a/tests/lean/match_bug.lean.expected.out b/tests/lean/match_bug.lean.expected.out new file mode 100644 index 000000000..5d7bfa785 --- /dev/null +++ b/tests/lean/match_bug.lean.expected.out @@ -0,0 +1 @@ +match_bug.lean:3:6: error: invalid occurrence of variable 'bar' in the left-hand-side of recursive equation