From 2487e3b83dd65c7032d5091cc85c3e7bc8837f48 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 29 Nov 2014 17:29:03 -0800
Subject: [PATCH] fix(frontends/lean/parser): user provided numeral notation
 should have precedence over the default based on 'num'

---
 src/frontends/lean/parser.cpp |  6 ++++--
 tests/lean/run/num_bug2.lean  | 13 +++++++++++++
 2 files changed, 17 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/num_bug2.lean

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index fc83b7d6b..618123593 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1167,10 +1167,12 @@ expr parser::parse_numeral_expr() {
                            "(solution: use 'import data.num', or define notation for the given numeral)", p);
     }
     buffer<expr> cs;
-    for (expr const & c : vals)
-        cs.push_back(copy_with_new_pos(c, p));
     if (*m_has_num)
         cs.push_back(save_pos(from_num(n), p));
+    for (expr const & c : vals)
+        cs.push_back(copy_with_new_pos(c, p));
+    // Remark: choices are processed from right to left.
+    // We want to process user provided notation before the default 'num'.
     lean_assert(!cs.empty());
     if (cs.size() == 1)
         return cs[0];
diff --git a/tests/lean/run/num_bug2.lean b/tests/lean/run/num_bug2.lean
new file mode 100644
index 000000000..b59f2157f
--- /dev/null
+++ b/tests/lean/run/num_bug2.lean
@@ -0,0 +1,13 @@
+import algebra.ring data.num
+open algebra
+
+variable A : Type
+variable s : ring A
+variable H0 : 0 = 0 -- since algebra defines notation '0' it should have precedence over num
+variable H1 : 1 = 1 -- since algebra defines notation '1' it should have precedence over num
+
+example : has_zero.zero A = has_zero.zero A :=
+H0
+
+example : has_one.one A = has_one.one A :=
+H1