lean2/tests/lua/env11.lua

37 lines
1.4 KiB
Lua
Raw Normal View History

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)