fix(frontends/lean): fix '#' override notation on the left-hand-side of recursive equations (and match-expressions)

src/frontends/lean/builtin_exprs.cpp

@@ -521,7 +521,7 @@ static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &
 static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_info const &) {
     name n = p.check_id_next("invalid '#' local notation, identifier expected");
     environment env = overwrite_notation(p.env(), n);
-    return p.parse_scoped_expr(0, nullptr, env);
+    return p.parse_expr_with_env(env);
 }
 
 static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info const & pos) {

src/frontends/lean/parser.cpp

@@ -1348,6 +1348,11 @@ expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environme
     return parse_expr(rbp);
 }
 
+expr parser::parse_expr_with_env(local_environment const & lenv, unsigned rbp) {
+    flet<environment> set_env(m_env, lenv);
+    return parse_expr(rbp);
+}
+
 static bool is_tactic_type(expr const & e) {
     return is_constant(e) && const_name(e) == get_tactic_name();
 }

src/frontends/lean/parser.h

@@ -402,6 +402,7 @@ public:
         return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp);
     }
     expr parse_scoped_expr(buffer<expr> const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
+    expr parse_expr_with_env(local_environment const & lenv, unsigned rbp = 0);
 
     expr parse_tactic(unsigned rbp = 0);
     expr parse_tactic_expr_arg(unsigned rbp = 0);

tests/lean/run/override_on_equations.lean

@@ -0,0 +1,24 @@
+open nat
+
+inductive expr :=
+| zero : expr
+| one  : expr
+| add  : expr → expr → expr
+
+namespace expr
+
+infix `+` := expr.add
+
+set_option pp.notation false
+
+definition ev : expr → nat
+| zero          := 0
+| one           := 1
+| #expr (a + b) := ev a + ev b
+
+definition foo : expr := add zero (add one one)
+
+example : ev foo = 2 :=
+rfl
+
+end expr