3.1 Terms

　termの例を挙げます．

`x+1`;;
val it : term = `x + 1`
`(x)+1`;;
val it : term = `x + 1`
` x + ( 1 ) `;;
val it : term = `x + 1`

これらはいずれも同じtermで，その内部表現は

# remove_printer print_qterm;;
`x+1`;;
val it : term =
...
# install_printer print_qterm;;

のように参照できます．
　代入は，subst関数を用いて

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

とします．なお

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

は駄目ですが，括弧を付けると

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

となります．