From 3726688711aa863b1a2f61003754c7fdf47afb2c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 May 2014 12:17:16 -0700 Subject: [PATCH] test(lua): add test to demonstrate the different between list(A) where A is a parameter, and where A is an index Signed-off-by: Leonardo de Moura --- tests/lua/ind4.lua | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 tests/lua/ind4.lua diff --git a/tests/lua/ind4.lua b/tests/lua/ind4.lua new file mode 100644 index 000000000..534ee9f21 --- /dev/null +++ b/tests/lua/ind4.lua @@ -0,0 +1,30 @@ +function display_type(env, t) + print(tostring(t) .. " : " .. tostring(env:normalize(env:type_check(t)))) +end + +local env = environment() +local l = param_univ("l") +local U_l = mk_sort(l) +local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop +local A = Local("A", U_l) +local list_l = Const("list", {l}) + +local env1 = add_inductive(env, + "list", {l}, 1, Pi(A, U_l1), + "nil", Pi(A, list_l(A)), + "cons", Pi(A, mk_arrow(A, list_l(A), list_l(A)))) + +display_type(env1, Const("list_rec", {1, 1})) + +-- Slightly different definition where A : Type.{l} is an index +-- instead of a global parameter +local U_sl = mk_sort(succ_univ(l)) +local env2 = add_inductive(env, + "list", {l}, 0, Pi(A, U_sl), -- The resultant type must live in the universe succ(l) + "nil", Pi(A, list_l(A)), + "cons", Pi(A, mk_arrow(A, list_l(A), list_l(A)))) +display_type(env2, Const("list_rec", {1, 1})) + + + +