From 3608826e4c6f5610e3cc35fe13ffad1f2a2c06a2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 May 2014 15:54:41 -0700 Subject: [PATCH] test(lua): add inductive decl serialization test Signed-off-by: Leonardo de Moura --- tests/lua/ind1.lua | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/tests/lua/ind1.lua b/tests/lua/ind1.lua index e8d4d3687..defc267bd 100644 --- a/tests/lua/ind1.lua +++ b/tests/lua/ind1.lua @@ -128,6 +128,13 @@ assert(tc:is_def_eq(length(nil_nat), zero)) assert(tc:is_def_eq(length(cons_nat(zero, nil_nat)), succ(zero))) assert(tc:is_def_eq(length(cons_nat(zero, cons_nat(zero, nil_nat))), succ(succ(zero)))) +env:export("ind1_mod.olean") +local env2 = import_modules("ind1_mod") +local tc = type_checker(env2) +assert(tc:is_def_eq(length(nil_nat), zero)) +assert(tc:is_def_eq(length(cons_nat(zero, nil_nat)), succ(zero))) +assert(tc:is_def_eq(length(cons_nat(zero, cons_nat(zero, nil_nat))), succ(succ(zero)))) + -- Martin-Lof style identity type local env = hott_environment() local Id_l = Const("Id", {l})