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

test(lua): add another add_inductive example

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-19 17:48:35 -07:00
parent 4f15240a71
commit eb6807e1d3
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
tests/lua/ind_ex.lua Normal file
View file

@ -0,0 +1,16 @@
local env = environment()
local l = param_univ("l")
local U_l = mk_sort(l)
local inhabited = Const("inhabited", {l})
local A = Local("A", U_l)
local a = Local("a", A)
env = add_inductive(env,
"inhabited", {l}, 1, mk_arrow(U_l, Bool),
"inhabited_intro", Pi({A, a}, inhabited(A)))
function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))
end
display_type(env, Const("inhabited_rec", {1, 1}))