fun : (int -> int) -> int -> int apply (f : int -> int) = (\(x : int) -> f (x) : int -> int) fun : int -> int succ (x : int) = x + 1 fun : (int -> int -> int) -> int -> int -> int apply2 (f : int -> int -> int) = (\(x : int) -> (\(y : int) -> f x y : int -> int) : int -> int -> int) fun : int -> int -> int addmul (x : int) = (\(y : int) -> x * y + y * x : int -> int) fun : (int -> int -> int -> int) -> int -> int -> int -> int apply3 (f : int -> int -> int -> int) = (\(x : int) -> (\(y : int) -> (\(z : int) -> f x y z : int -> int) : int -> int) : int -> int -> int -> int) let conj : int -> int -> int -> int = (\(x : int) -> (\(y : int) -> (\(z : int) -> x * y * z : int -> int) : int -> int -> int) : int -> int -> int -> int) let main : int = apply succ (-1) + apply2 addmul 3 7 + apply3 conj 0 1 2