michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lua): add tests for expr object

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-11 13:11:31 -08:00
parent 8dd85ebc15
commit bdc23fba32
1 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
tests/lua/expr5.lua Normal file
View file

@ -0,0 +1,22 @@
e = context_entry("a", Const("a"))
n = e:get_body()
check_error(function() mk_eq(n, Const("a")) end)
print(Const("a") < Const("b"))
check_error(function() mk_app(Const("a")) end)
print(mk_eq(Const("a"), Const("b")))
print(mk_pi("x", Const("N"), Var(0)))
print(Pi("x", Const("N"), Const("x")))
assert(mk_pi("x", Const("N"), Var(0)) == Pi("x", Const("N"), Const("x")))
assert(mk_let("x", Const("a"), Var(0)) == Let("x", Const("a"), Const("x")))
print(mk_let("x", Const("N"), Const("a"), Var(0)))
check_error(function() Pi({"x"}, Const("x")) end)
check_error(function() Pi({"x", Const("N")}, Const("x")) end)
check_error(function() Pi({{"x"}}, Const("x")) end)
check_error(function() Pi(Const("x")) end)
check_error(function() Pi(Const("x"), Const("N"), Const("x"), Const("a")) end)
check_error(function() Pi({}, Const("x")) end)