16 lines
586 B
Lua
16 lines
586 B
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))))
|