読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

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.
<