From 69f6930bd70dbb90ef1edf217fdeaf5074bf754c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 May 2014 11:26:02 -0700 Subject: [PATCH] test(lua): add Acc datatype declaration test Signed-off-by: Leonardo de Moura --- tests/lua/ac.lua | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/lua/ac.lua diff --git a/tests/lua/ac.lua b/tests/lua/ac.lua new file mode 100644 index 000000000..216b75618 --- /dev/null +++ b/tests/lua/ac.lua @@ -0,0 +1,17 @@ +local env = environment() +local l = param_univ("l") +local U_l = mk_sort(l) +local A = Local("A", U_l) +local R = Local("R", mk_arrow(A, A, Bool)) +local Acc = Const("Acc", {l}) +local x = Local("x", A) +local y = Local("y", A) +env = add_inductive(env, + "Acc", {l}, 2, Pi({A, R, x}, Bool), + "Acc_intro", Pi({A, R, x}, mk_arrow(Pi(y, mk_arrow(R(y, x), Acc(A, R, y))), Acc(A, R, x)))) + +function display_type(env, t) + print(tostring(t) .. " : " .. tostring(type_checker(env):infer(t))) +end + +display_type(env, Const("Acc_rec", {1}))