第 1 回
Coq のインストール，関数，大域的変数， Specification の定義

• プリント

• Coq，ProofGeneral のインストール
  浅井研の Wiki ( http://dellsv/wiki/) の Coq，Proofgeneral のインストールのページ参照
• 12. 式 : 型 : ソート
  直感的には，型の型がソート
  (例)

   式 :     型     : ソート
    1 : nat
        nat -> nat : Set