michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lua): add section+inductive_family test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-02 13:07:13 -07:00
parent 6ee272477a
commit 2a101657c8
1 changed files with 39 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
tests/lua/sect8.lua Normal file
View file

@ -0,0 +1,39 @@
local env = environment()
env = env:begin_section_scope()
local nat = Const("nat")
env = add_inductive(env,
"nat", Type,
"zero", nat,
"succ", mk_arrow(nat, nat))
local zero = Const("zero")
local succ = Const("succ")
env = env:begin_section_scope()
env = env:add_global_level("l")
local l = mk_global_univ("l")
env = env:add(check(env, mk_var_decl("A", mk_sort(l))), binder_info(true))
env = env:add(check(env, mk_var_decl("B", mk_sort(l))), binder_info(true))
local A = Const("A")
local vector = Const("vector")
local n = Local("n", nat)
env = add_inductive(env,
"vector", mk_arrow(nat, mk_sort(max_univ(l, 1))),
"nil", vector(zero),
"cons", Pi(n, mk_arrow(A, vector(n), vector(succ(n)))))
print(env:find("vector_rec"):type())
assert(env:find("cons"):type() == Pi(n, mk_arrow(A, vector(n), vector(succ(n)))))
env = env:end_scope()
print(env:find("vector_rec"):type())
print(env:find("cons"):type())
local l = mk_param_univ("l")
local A = Local("A", mk_sort(l))
local vector = Const("vector", {l})
assert(env:find("cons"):type() == Pi({A, n}, mk_arrow(A, vector(A, n), vector(A, succ(n)))))
env = env:end_scope()
print(env:find("vector_rec"):type())
print(env:find("cons"):type())
env:export("sect8_mod.olean")
local env2 = import_modules("sect8_mod")
assert(env:find("vector_rec"):type() == env2:find("vector_rec"):type())