fix(frontends/lean/notation_cmd): fixes #808

This commit and 2b1d2c fixes #808

src/frontends/lean/notation_cmd.cpp

@@ -42,6 +42,7 @@ static unsigned parse_precedence_core(parser & p) {
         environment env = open_prec_aliases(open_num_notation(p.env()));
         parser::local_scope scope(p, env);
         expr val = p.parse_expr(get_max_prec());
+        val = elim_choice_num(val);
         val = normalize(p.env(), val);
         if (optional<mpz> mpz_val = to_num(val)) {
             if (!mpz_val->is_unsigned_int())

src/frontends/lean/util.cpp

@@ -467,6 +467,10 @@ class elim_choice_num_fn : public replace_visitor {
     }
 };
 
+expr elim_choice_num(expr const & e) {
+    return elim_choice_num_fn()(e);
+}
+
 optional<unsigned> parse_priority(parser & p) {
     if (p.curr_is_token(get_priority_tk())) {
         p.next();
@@ -476,7 +480,7 @@ optional<unsigned> parse_priority(parser & p) {
         expr val = p.parse_expr();
         // Remark: open_num_notation will not override numeral overloading.
         // So, we use the following helper class for eliminating it.
-        val = elim_choice_num_fn()(val);
+        val = elim_choice_num(val);
         val = normalize(p.env(), val);
         if (optional<mpz> mpz_val = to_num(val)) {
             if (!mpz_val->is_unsigned_int())

src/frontends/lean/util.h

@@ -110,6 +110,9 @@ char const * close_binder_string(binder_info const & bi, bool unicode);
 /** \brief Cleanup expression after elaboration. */
 expr postprocess(environment const & env, expr const & e);
 
+/** Replaces every (choice a_0 ... a_n), where a_0 is a numeral, with a_0. */
+expr elim_choice_num(expr const & e);
+
 /** \brief Parse `[priority <num>]`. Return none if current token is not `[priority` */
 optional<unsigned> parse_priority(parser & p);
 

tests/lean/run/808.lean

@@ -0,0 +1,9 @@
+notation 1 := eq
+
+postfix `x`:(max+1) := eq
+
+postfix [priority 1] `y`:max := eq
+
+definition foo [instance] [priority 1] : inhabited nat := inhabited.mk nat.zero
+
+definition bar [unfold 1] := @eq