3.2 Types

　ところが

subst[`2`,`x`]`x+1`;;
Warning: inventing type variables
val it : term = `x + 1`

のように上手く行きません．このWarningはterm xのhol_type（というOCamlでのtype）が不明ということなので，例えば，num（自然数，非負整数）と明示すれば

subst[`2`,`(x:num)`]`x+1`;;
val it : term = `2 + 1`

となります．前回，x+1の代入のときに何も言われなかったのは「hol_typeがnumであるterm 1との和を考えているので，trem xのhol_typeもnumである」という推量が働いていたからです．
　termのhol_typeを確認するには，termを受け取りそのhol_typeを返すtype_of関数を用いて

type_of`1`;;
val it : hol_type = `:num`
type_of`x+1`;;
val it : hol_type = `:num`
type_of`x`;;
Warning: inventing type variables
val it : hol_type = `:?80029`
type_of`(x:num)`;;
val it : hol_type = `:num`
type_of`(&1:int)`;;
val it : hol_type = `:int`
type_of`&1`;;
val it : hol_type = `:real`
type_of`x+(&1)`;;
val it : hol_type = `:real`
type_of`(x:real)+y`;;
val it : hol_type = `:real`

のようにします．ここで，intは整数，realは有理数を表すhol_typeであり，&記号を付いた数はデフォルトではrealになることに注意します．また

`&1+&2`;;
Exception: Failure "typechecking error (overload resolution)".`

のように書くと，+と&とが結合してしまうので，上記のように括弧を付けて&1+(&2)とするか，+と&との間にスペースが必要です．
　なお，集合として包含関係があっても，異なるhol_typeのterm間の計算はできません．