T:Type{i}, U:Type{j}, V:Type{k}, f:(T
U
V). f = uncurry curry fT:Type{i}, U:Type{j}, V:Type{k}, f:(TUV). f = curry uncurry f
x,y. y(x(x,y)))(x,y. y(x(x,y)))
(f) == (x.f(y.x(x,y)))(x.f(y.x(x,y)))| def | curry | curry f(x,y) == f( < x,y > ) |
| def | uncurry | uncurry f(x) == x/l,r. f(l,r) |
| THM | curry_uncurry_inverse | T:Type{i}, U:Type{j}, V:Type{k}, f:(TUV). f = uncurry curry f |
| THM | uncurry_curry_inverse | T:Type{i}, U:Type{j}, V:Type{k}, f:(TUV). f = curry uncurry f |
| def | letrec | (rec) (letrec f b(f)) == b((letrec f b(f)) ) |
| def | letrec_body | = b == b |
| def | letrec_arg | x b(x) (x) == b(x) |
| def | theta | T == (x,y. y(x(x,y)))(x,y. y(x(x,y))) |
| def | applicative_Y | Y(f) == (x.f(y.x(x,y)))(x.f(y.x(x,y))) |