lean2/tests/lua/explicit.lua
Leonardo de Moura 3169f8c126 feat(library): add mk_explicit/is_explicit procedures for '@'-expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-24 12:11:27 -07:00

7 lines
224 B
Lua

local f = Const("f")
local a = Const("a")
print(mk_explicit(f)(a))
assert(is_explicit(mk_explicit(f)))
assert(not is_explicit(f))
assert(get_explicit_arg(mk_explicit(f)) == f)
check_error(function() get_explicit_arg(f) end)