From a72be5eea4bc226a06bce4ea5a154c56a27edf37 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 May 2014 17:06:19 -0700 Subject: [PATCH] test(lua): add example suggested by Cody Signed-off-by: Leonardo de Moura --- tests/lua/ind_tricky.lua | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/lua/ind_tricky.lua diff --git a/tests/lua/ind_tricky.lua b/tests/lua/ind_tricky.lua new file mode 100644 index 0000000000..27dce38014 --- /dev/null +++ b/tests/lua/ind_tricky.lua @@ -0,0 +1,17 @@ +local env = environment() + +local tricky = Const("tricky") +local P = Const("P") + +env = add_inductive(env, + "tricky", Bool, + "C", mk_arrow(Pi(P, Bool, mk_arrow(P, P)), tricky)) + +function display_type(env, t) + print(tostring(t) .. " : " .. tostring(type_checker(env):check(t))) +end + +env = env:add_global_level("u") +local tricky_rec = Const("tricky_rec", {0}) + +display_type(env, tricky_rec)