From cfa9520655bb8bf8a19179f26f10c667155a0f0b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 May 2014 08:49:09 -0700 Subject: [PATCH] test(lua): add more level API unit tests Signed-off-by: Leonardo de Moura --- tests/lua/level5.lua | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 tests/lua/level5.lua diff --git a/tests/lua/level5.lua b/tests/lua/level5.lua new file mode 100644 index 000000000..52f06a698 --- /dev/null +++ b/tests/lua/level5.lua @@ -0,0 +1,14 @@ +local l1 = mk_param_univ("l1") +assert(l1:is_param()) +local m = mk_meta_univ("m") +assert(m:is_meta()) +assert(mk_level_zero():is_explicit()) +assert(mk_level_one():is_explicit()) +local t1 = mk_level_max(l1, mk_level_one()) +assert(t1:has_param()) +local t2 = mk_level_imax(mk_level_one(), l1) +assert(t2:is_imax()) +assert(not pcall(function() t2:id() end)) +assert(not pcall(function() l1:lhs() end)) +assert(not pcall(function() l1:rhs() end)) +assert(not pcall(function() l1:succ_of() end))