From 1447d7e7657eee6d72230fcfc8b41cc4472c648b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 May 2014 10:52:58 -0700 Subject: [PATCH] test(lua): add another inductive datatype example Signed-off-by: Leonardo de Moura --- tests/lua/ind6.lua | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/lua/ind6.lua diff --git a/tests/lua/ind6.lua b/tests/lua/ind6.lua new file mode 100644 index 000000000..ba84b5bab --- /dev/null +++ b/tests/lua/ind6.lua @@ -0,0 +1,18 @@ + +local env = environment() +local u = param_univ("u") +local Set = Const("Set", {u}) +local A = Local("A", mk_sort(u)) + +env = add_inductive(env, + "Set", {u}, 0, mk_sort(u+1), + "sup", Pi(A, mk_arrow(mk_arrow(A, Set), Set))) + +local env = environment() +local u = param_univ("u") +local Set = Const("Set", {u}) +local A = Local("A", mk_sort(u)) + +env = add_inductive(env, + "Set", {u}, 1, Pi(A, mk_sort(u+1)), + "sup", Pi(A, mk_arrow(mk_arrow(A, Set(A)), Set(A))))