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

test(lua): add test to demonstrate the different between list(A) where A is a parameter, and where A is an index

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-20 12:17:16 -07:00
parent 11fc917102
commit 3726688711
1 changed files with 30 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
tests/lua/ind4.lua Normal file
View file

@ -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}))