lean2/tests/lua/eta.lua

local env = bare_environment()
env = add_decl(env, mk_var_decl("f", mk_arrow(Bool, mk_arrow(Bool, Bool))))
local f   = Const("f")
local x   = Local("x", Bool)
local y   = Local("y", Bool)
local z   = Local("z", Bool)
local tc  = type_checker(env)
print(tc:whnf(Fun(x, f(x))))
print(tc:whnf(Fun(x, y, f(x, y))))
print(tc:whnf(Fun(x, y, f(Const("a"), y))))
print(tc:whnf(Fun(z, x, y, f(z, y))))
assert(tc:is_def_eq(f, Fun(x, f(x))))
assert(tc:is_def_eq(f, Fun(x, y, f(x, y))))
local A = Const("A")
local a = Local("a", A)
assert(tc:is_def_eq(Fun(a, a)(f), Fun(x, y, f(x, y))))
refactor(library/kernel_bindings): rename empty_environment ==> bare_environment in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-05-21 18:24:24 +00:00			`local env = bare_environment()`
refactor(kernel/converter): implement eta in whnf instead of is_def_eq. Without cumulativity, we do not have problems with Eta at whnf anymore. When we had cumulativity, we could not not simply reduce (fun x : A, f x) ==> f This step is correct only if domain(f) was definitionally equal to f. Here is a problematic example for systems with cumulativity Given, f : Type.{2} -> Bool (fun x : Type.{1}, f x) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-05-13 00:49:51 +00:00			`env = add_decl(env, mk_var_decl("f", mk_arrow(Bool, mk_arrow(Bool, Bool))))`
			`local f = Const("f")`
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 x = Local("x", Bool)`
			`local y = Local("y", Bool)`
			`local z = Local("z", Bool)`
refactor(kernel/converter): implement eta in whnf instead of is_def_eq. Without cumulativity, we do not have problems with Eta at whnf anymore. When we had cumulativity, we could not not simply reduce (fun x : A, f x) ==> f This step is correct only if domain(f) was definitionally equal to f. Here is a problematic example for systems with cumulativity Given, f : Type.{2} -> Bool (fun x : Type.{1}, f x) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-05-13 00:49:51 +00:00			`local tc = type_checker(env)`
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			`print(tc:whnf(Fun(x, f(x))))`
			`print(tc:whnf(Fun(x, y, f(x, y))))`
			`print(tc:whnf(Fun(x, y, f(Const("a"), y))))`
			`print(tc:whnf(Fun(z, x, y, f(z, y))))`
			`assert(tc:is_def_eq(f, Fun(x, f(x))))`
			`assert(tc:is_def_eq(f, Fun(x, y, f(x, y))))`
refactor(kernel/converter): implement eta in whnf instead of is_def_eq. Without cumulativity, we do not have problems with Eta at whnf anymore. When we had cumulativity, we could not not simply reduce (fun x : A, f x) ==> f This step is correct only if domain(f) was definitionally equal to f. Here is a problematic example for systems with cumulativity Given, f : Type.{2} -> Bool (fun x : Type.{1}, f x) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-05-13 00:49:51 +00:00			`local A = Const("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 a = Local("a", A)`
			`assert(tc:is_def_eq(Fun(a, a)(f), Fun(x, y, f(x, y))))`