lean2/tests/lua/eta.lua

local env = bare_environment()
env = add_decl(env, mk_constant_assumption("f", mk_arrow(Prop, mk_arrow(Prop, Prop))))
local f   = Const("f")
local x   = Local("x", Prop)
local y   = Local("y", Prop)
local z   = Local("z", Prop)
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 11:24:24 -07:00			`local env = bare_environment()`
refactor(kernel): rename var_decl to constant_assumption Motivation: it matches the notation used to declare it. 2014-10-02 16:54:56 -07:00			`env = add_decl(env, mk_constant_assumption("f", mk_arrow(Prop, mk_arrow(Prop, Prop))))`
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-12 17:49:51 -07:00			`local f = Const("f")`
refactor(*): rename Bool to Prop Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-22 09:43:18 -07:00			`local x = Local("x", Prop)`
			`local y = Local("y", Prop)`
			`local z = Local("z", Prop)`
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-12 17:49:51 -07: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 09:14:55 -07: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-12 17:49:51 -07: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 09:14:55 -07:00			`local a = Local("a", A)`
			`assert(tc:is_def_eq(Fun(a, a)(f), Fun(x, y, f(x, y))))`