lean2/tests/lua/env11.lua

local A     = Const("A")
local B     = Const("B")
local env   = environment()
local env1  = add_decl(env, mk_constant_assumption("A", Prop))
env1  = add_decl(env1, mk_constant_assumption("B", Prop))
env1  = add_decl(env1, mk_axiom("H", B))
local c1    = check(env1, mk_axiom("H1", A))
local c2    = check(env1, mk_axiom("H2", A))
local env1b = env1:add(c1)
local env2  = env1b:add(c2)
local c3    = check(env2, mk_theorem("H3", A, Const("H1")))
function expected_error(f)
   ok, ex = pcall(f)
   assert(not ok)
   print("expected error: " .. ex:what())
end

expected_error(function() env1:add(c3) end)
expected_error(function() env2:add(c1) end)
env3 = env2:add_universe("u")
expected_error(function() env3:add_universe("u") end)
expected_error(function() check(env2, mk_theorem("H1", A, Const("H1"))) end)
local c4   = check(env1b, mk_theorem("H2", A, Const("H1")))
expected_error(function() env3:add(c4) end)
env3 = env3:replace(c4)
assert(env2:find("H2"):is_axiom())
assert(not env3:find("H2"):is_axiom())
assert(env3:find("H2"):is_theorem())
local c5   = check(env1b, mk_theorem("H5", A, Const("H1")))
expected_error(function() env3:replace(c5) end)
local c6   = check(env, mk_definition("A", Type, Prop))
expected_error(function() env3:replace(c6) end)
local c7   = check(env1b, mk_definition("H2", A, Const("H1")))
expected_error(function() env2:replace(c7) end)
local c8   = check(env1b, mk_theorem("H2", B, Const("H")))
expected_error(function() env2:replace(c8) end)