lean2/tests/lua/proof_state1.lua

28 lines
689 B
Lua
Raw Normal View History

local ps = proof_state()
local env = environment()
local Bool = Const("Bool")
env:add_var("p", Bool)
env:add_var("q", Bool)
local p, q = Consts("p, q")
local ctx = context()
ctx = ctx:extend("H1", p)
ctx = ctx:extend("H2", q)
ps = to_proof_state(env, ctx, p)
print(ps)
for n, g in ps:goals():pairs() do
assert(is_goal(g))
print(n, g)
end
assert(#(ps:goals()) == 1)
assert(ps:goals():tail():is_nil())
assert(ps:goals():head() == name("main"))
assert(not ps:goals():empty())
assert(ps:precision() == precision.Precise)
local menv = ps:menv()
local pb = ps:proof_builder()
local cb = ps:cex_builder()
assert(not ps:is_proof_final_state())
assert(not ps:is_cex_final_state())