From 3ea09daf441345c71b95a55bd0fe9750219654cf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Dec 2013 17:46:56 -0800
Subject: [PATCH] fix(frontends/lean/frontend): is_coercion for environment
 objects that have parents

Bug was exposed by tests/lua/coercion_bug1.lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/frontend.cpp |  5 ++++-
 tests/lua/coercion_bug1.lua     | 23 +++++++++++++++++++++++
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 tests/lua/coercion_bug1.lua

diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index a651e5b2c..b691f3ee2 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -339,7 +339,10 @@ struct lean_extension : public environment::extension {
     }
 
     bool is_coercion(expr const & f) const {
-        return m_coercion_set.find(f) != m_coercion_set.end();
+        if (m_coercion_set.find(f) != m_coercion_set.end())
+            return true;
+        lean_extension const * parent = get_parent();
+        return parent && parent->is_coercion(f);
     }
 };
 
diff --git a/tests/lua/coercion_bug1.lua b/tests/lua/coercion_bug1.lua
new file mode 100644
index 000000000..2d37ce2c1
--- /dev/null
+++ b/tests/lua/coercion_bug1.lua
@@ -0,0 +1,23 @@
+local env = environment()
+
+parse_lean_cmds([[
+  Variable f : Int -> Int -> Int
+  Notation 20 _ +++ _ : f
+  Show f 10 20
+  Notation 20 _ --- _ : f
+  Show f 10 20
+]], env)
+
+local F = parse_lean('f 10 20', env)
+print(lean_formatter(env)(F))
+assert(tostring(lean_formatter(env)(F)) == "10 --- 20")
+
+local child = env:mk_child()
+
+parse_lean_cmds([[
+  Show f 10 20
+]], child)
+
+assert(tostring(lean_formatter(env)(F)) == "10 --- 20")
+print(lean_formatter(child)(F))
+assert(tostring(lean_formatter(child)(F)) == "10 --- 20")