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

test(lua): add Acc datatype declaration test

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-23 11:26:02 -07:00
parent b68b9ccc05
commit 69f6930bd7
1 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
tests/lua/ac.lua Normal file
View file

@ -0,0 +1,17 @@
local env = environment()
local l = param_univ("l")
local U_l = mk_sort(l)
local A = Local("A", U_l)
local R = Local("R", mk_arrow(A, A, Bool))
local Acc = Const("Acc", {l})
local x = Local("x", A)
local y = Local("y", A)
env = add_inductive(env,
"Acc", {l}, 2, Pi({A, R, x}, Bool),
"Acc_intro", Pi({A, R, x}, mk_arrow(Pi(y, mk_arrow(R(y, x), Acc(A, R, y))), Acc(A, R, x))))
function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):infer(t)))
end
display_type(env, Const("Acc_rec", {1}))