lean2/tests/lua/eta.lua

local env = bare_environment()
env = add_decl(env, mk_var_decl("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))))