From fcf94ad7c2b7904d68bf6b580b2705efe70af19d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 May 2014 20:12:55 -0700 Subject: [PATCH] test(lua): add test for inductive datatype positivity check Signed-off-by: Leonardo de Moura --- tests/lua/ind1.lua | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/lua/ind1.lua b/tests/lua/ind1.lua index f54f55ff6c..5daf2c27e4 100644 --- a/tests/lua/ind1.lua +++ b/tests/lua/ind1.lua @@ -70,3 +70,9 @@ env = add_inductive(env, {}, "succ_odd", Pi(b, Nat, mk_arrow(Odd(b), Even(succ(b))))}, {"Odd", mk_arrow(Nat, Bool), "succ_even", Pi(b, Nat, mk_arrow(Even(b), Odd(succ(b))))}) + +local flist_l = Const("flist", {l}) +env = add_inductive(env, + "flist", {l}, 1, mk_arrow(U_l, U_l1), + "fnil", Pi({{A, U_l, true}}, flist_l(A)), + "fcons", Pi({{A, U_l, true}}, mk_arrow(A, mk_arrow(Nat, flist_l(A)), flist_l(A))))