lean2/tests/lua/expr8.lua

local Or = Const("or")
local A  = Local("A", Type)
local a  = Local("a", A, binder_info(true))
local b  = Local("b", A)
local H  = Local("H", Or(a, b), binder_info(false, true))
print(Pi(A, a, b, H, Or(b, a)))
print(Fun(A, a, b, H, Or(b, a)))
test(lua): add tests for new Pi/Fun notation in Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-05-20 00:17:15 +00:00			`local Or = Const("or")`
			`local A = Local("A", Type)`
refactor(kernel): store binder_infor in local constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-30 16:14:55 +00:00			`local a = Local("a", A, binder_info(true))`
test(lua): add tests for new Pi/Fun notation in Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-05-20 00:17:15 +00:00			`local b = Local("b", A)`
refactor(kernel): store binder_infor in local constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-06-30 16:14:55 +00:00			`local H = Local("H", Or(a, b), binder_info(false, true))`
			`print(Pi(A, a, b, H, Or(b, a)))`
			`print(Fun(A, a, b, H, Or(b, a)))`