37 lines
930 B
Text
37 lines
930 B
Text
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 -> 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
|
|
|
|
|
|
|