5.1 Curried functions
(+);;
val it : int -> int -> int =
同じく，HOL Lightの加法の演算子のhol_typeを見ると
type_of `(+)`;;
val it : hol_type = `:num->num->num`
のようと表示されます．これは例えば「x+1」が，x に対して「引数 -> x+引数」という中間の関数を対応させ，その中間の関数による 1 の像として得られることを意味しており，このことは
type_of `(+) x`;;
val it : hol_type = `:num->num`
type_of `(+) x 1`;;
val it : hol_type = `:num`
とすれば確認でき，この内部書式のままの入力でも
`(+) x 1`;;
val it : term = `x + 1`
`(==>) ((=) ((+) x y) z) (P z)`;;
val it : term = `x + y = z ==> P z`
のように出力はこれまで通りのスタイルになります．
なお，こうした１変数関数への分解は，論理学者Haskell Curryの名から，currying（カリー化）と呼ばれています．
