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

fix(library/scope): bug in add_definition

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-02 11:04:34 -07:00
parent e56307f006
commit 936ca80b9b
2 changed files with 29 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/scope.cpp
View file

@ -184,10 +184,10 @@ public:
if (d.is_definition()) {
declaration new_d = mk_definition(d.get_name(), new_ls, new_type, new_value, d.is_opaque(),
d.get_weight(), d.get_module_idx(), d.use_conv_opt());
m_env = module::add(m_env, check(m_env, new_d));
m_env = add(m_env, check(m_env, new_d));
} else {
declaration new_d = mk_theorem(d.get_name(), new_ls, new_type, new_value);
m_env = module::add(m_env, check(m_env, new_d));
m_env = add(m_env, check(m_env, new_d));
}
}
};

27
tests/lua/sect6.lua Normal file
View file

@ -0,0 +1,27 @@
local env = environment()
env = env:begin_section_scope()
env = env:begin_section_scope()
env = env:add_global_level("l")
local l = mk_global_univ("l")
env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true))
local A = Const("A")
env = add_decl(env, mk_var_decl("R", mk_arrow(A, A, Bool)))
local R = Const("R")
local a = Local("a", A)
env = add_decl(env, mk_definition("reflexive", Bool, Pi(a, R(a, a))))
env = add_decl(env, mk_definition("id", mk_arrow(A, A), Fun(a, a)))
env = env:end_scope()
local A1 = Local("A", mk_sort(mk_param_univ("l")))
local R1 = Local("R", mk_arrow(A1, A1, Bool))
local a1 = Local("a", A1)
print(env:find("reflexive"):type())
print(env:find("reflexive"):value())
assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool))
assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1))))
print(env:find("id"):type())
print(env:find("id"):value())
env = env:end_scope()
print(env:find("reflexive"):type())
print(env:find("reflexive"):value())
assert(env:find("reflexive"):type() == Pi({A1, R1}, Bool))
assert(env:find("reflexive"):value() == Fun({A1, R1}, Pi(a1, R1(a1, a1))))