From c84e886c7be3ef3d9c853b1ded0001572554e19e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 31 Aug 2015 18:05:58 -1000
Subject: [PATCH] fix(frontends/lean/notation_cmd): fixes #808

This commit and 2b1d2c fixes #808
---
 src/frontends/lean/notation_cmd.cpp | 1 +
 src/frontends/lean/util.cpp         | 6 +++++-
 src/frontends/lean/util.h           | 3 +++
 tests/lean/run/808.lean             | 9 +++++++++
 4 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/808.lean

diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index cb0c52ecd..544ec229f 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/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())
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 5f23d119e..abd39a26d 100644
--- a/src/frontends/lean/util.cpp
+++ b/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())
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index b4170f044..1d93162a0 100644
--- a/src/frontends/lean/util.h
+++ b/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);
 
diff --git a/tests/lean/run/808.lean b/tests/lean/run/808.lean
new file mode 100644
index 000000000..7d53c9751
--- /dev/null
+++ b/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