15 lines
423 B
Lua
15 lines
423 B
Lua
|
local pb = proof_builder(function(m, a)
|
||
|
|
return m:find("main")
|
||
|
|
end)
|
||
|
|
assert(is_proof_builder(pb))
|
||
|
|
local a = assignment()
|
||
|
|
assert(is_assignment(a))
|
||
|
|
local m = proof_map()
|
||
|
|
assert(#m == 0)
|
||
|
|
assert(is_proof_map(m))
|
||
|
|
m:insert("main", Const("H"))
|
||
|
|
m:insert("subgoal", Const("H1"))
|
||
|
|
m:erase("subgoal")
|
||
|
|
assert(not pcall(function() m:find("subgoal") end))
|
||
|
|
assert(pb(m, a) == Const("H"))
|