HOL Lightにおいて等式は，数学におけるそれよりも特に基本的です．例えば，Iffは=記号にしても構いません．ただし，結合の強さと向き，typeの推量機能のため，時に括弧が必要です． `p /\ x = 1 q`;; val it : term = `p /\ x = 1 q` `p /\ x = 1 = q`;; va…

curringは，OCamlの殆ど，HOL Lightの全ての中置き２項演算子に使われていますが，順序対がないわけではなく，OCaml，HOL Light，それぞれにおいて # 1,2;; val it : int * int = (1, 2) # type_of `1,2`;; val it : hol_type = `:num#num` のようになってい…

例えば，OCamlの加法演算子を引数なしで呼ぶと (+);; val it : int -> int -> int = 同じく，HOL Lightの加法の演算子のhol_typeを見ると type_of `(+)`;; val it : hol_type = `:num->num->num` のようと表示されます．これは例えば「x+1」が，x に対して「…