diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index a79b5fc60..7d0f25efe 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -152,17 +152,20 @@ expr parser_imp::parse_postfix(expr const & left, operator_info const & op, pos_ /** \brief Parse a user defined infix operator. */ expr parser_imp::parse_infix(expr const & left, operator_info const & op, pos_info const & op_pos) { - return mk_application(op, op_pos, {left, parse_expr(op.get_precedence()+1)}); + expr right = parse_expr(op.get_precedence()+1); + return mk_application(op, op_pos, {left, right}); } /** \brief Parse a user defined infix-left operator. */ expr parser_imp::parse_infixl(expr const & left, operator_info const & op, pos_info const & op_pos) { - return mk_application(op, op_pos, {left, parse_expr(op.get_precedence())}); + expr right = parse_expr(op.get_precedence()); + return mk_application(op, op_pos, {left, right}); } /** \brief Parse a user defined infix-right operator. */ expr parser_imp::parse_infixr(expr const & left, operator_info const & op, pos_info const & op_pos) { - return mk_application(op, op_pos, {left, parse_expr(op.get_precedence()-1)}); + expr right = parse_expr(op.get_precedence()-1); + return mk_application(op, op_pos, {left, right}); } /** diff --git a/tests/lean/leak1.lean b/tests/lean/leak1.lean new file mode 100644 index 000000000..32e929928 --- /dev/null +++ b/tests/lean/leak1.lean @@ -0,0 +1 @@ +print 2 * a \ No newline at end of file diff --git a/tests/lean/leak1.lean.expected.out b/tests/lean/leak1.lean.expected.out new file mode 100644 index 000000000..93446efe4 --- /dev/null +++ b/tests/lean/leak1.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +leak1.lean:1:11: error: unknown identifier 'a' diff --git a/tests/lean/leak2.lean b/tests/lean/leak2.lean new file mode 100644 index 000000000..160778679 --- /dev/null +++ b/tests/lean/leak2.lean @@ -0,0 +1 @@ +print true /\ a \ No newline at end of file diff --git a/tests/lean/leak2.lean.expected.out b/tests/lean/leak2.lean.expected.out new file mode 100644 index 000000000..4010e4317 --- /dev/null +++ b/tests/lean/leak2.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +leak2.lean:1:15: error: unknown identifier 'a' diff --git a/tests/lean/leak3.lean b/tests/lean/leak3.lean new file mode 100644 index 000000000..e67141864 --- /dev/null +++ b/tests/lean/leak3.lean @@ -0,0 +1 @@ +print true = a \ No newline at end of file diff --git a/tests/lean/leak3.lean.expected.out b/tests/lean/leak3.lean.expected.out new file mode 100644 index 000000000..02d0fe1b4 --- /dev/null +++ b/tests/lean/leak3.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +leak3.lean:1:14: error: unknown identifier 'a'