michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/frontend): is_coercion for environment objects that have parents

Browse source 
Bug was exposed by tests/lua/coercion_bug1.lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-08 17:46:56 -08:00
parent 2a80807fef
commit 3ea09daf44
2 changed files with 27 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/frontend.cpp
View file

@ -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);
}
};

23
tests/lua/coercion_bug1.lua Normal file
View file

@ -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")