lean2/tests/lua/context1.lua
Leonardo de Moura ad2de3b53c feat(lua): expose level objects in the Lua bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-08 17:08:24 -08:00

25 lines
656 B
Lua

c = context()
assert(c:is_empty())
print(c)
e = context_entry("x", Const("N"))
assert(e:get_name() == name("x"))
assert(e:get_domain() == Const("N"))
assert(e:get_body():is_null())
print(e:get_body())
c = context(c, e)
print(c)
assert(not c:is_empty())
c = context(c, "y", Const("M"))
assert(#c == 2)
assert(c:size() == 2)
e, c1 = lookup(c, 0)
assert(c1:size() == 1)
assert(e:get_name() == name("y"))
c = context(c, "z", Const("N"), Const("a"))
print(c)
check_error(function() lookup(c, 10) end)
assert(lookup(c, 0):get_body() == Const("a"))
assert(not is_context_entry(c))
assert(is_context(c))
assert(is_context_entry(e))
assert(not is_context_entry(c))