From 8a44dfc1df51c7a0d7410ca339385d717295e6b8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Oct 2014 18:58:27 -0700
Subject: [PATCH] fix(frontends/lean/pp): bug in pretty printer notation match
 procedure

---
 src/frontends/lean/pp.cpp              | 2 ++
 tests/lean/notation6.lean              | 9 +++++++++
 tests/lean/notation6.lean.expected.out | 5 +++++
 3 files changed, 16 insertions(+)
 create mode 100644 tests/lean/notation6.lean
 create mode 100644 tests/lean/notation6.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 1afa640b4..4b74868ef 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -612,6 +612,8 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
     } else if (is_placeholder(p)) {
         return true;
     } else if (is_constant(p) && is_constant(e)) {
+        if (const_name(p) != const_name(e))
+            return false;
         levels p_ls = const_levels(p);
         levels e_ls = const_levels(p);
         while (!is_nil(p_ls)) {
diff --git a/tests/lean/notation6.lean b/tests/lean/notation6.lean
new file mode 100644
index 000000000..bd1eea649
--- /dev/null
+++ b/tests/lean/notation6.lean
@@ -0,0 +1,9 @@
+import logic data.num
+open num
+notation `o` := 10
+check 11
+constant f : num → num
+check o + 1
+check f o + o + o
+eval 9 + 1
+eval o+4
diff --git a/tests/lean/notation6.lean.expected.out b/tests/lean/notation6.lean.expected.out
new file mode 100644
index 000000000..84a39dc83
--- /dev/null
+++ b/tests/lean/notation6.lean.expected.out
@@ -0,0 +1,5 @@
+11 : num
+o + 1 : num
+f o + o + o : num
+o
+14