Variableコマンドと抽象化

Variable

この記事は途中です。
Variableコマンドを使って変数名とその型だけを宣言して使うことができる。
OCamlのsig型のようなものが簡単に記述できるような感じだ。

文法 [Variable 変数名 : 型.]

例えば、次の様に書くことができる。

Variable A : Set.
Variable B : Set.
Variable f : A -> B.

Fixpoint list_map (l:list A) : list B :=
  match l with
  | nil => nil
  | cons hd tl => cons (f hd) (list_map tl)
  end.


    

    <