最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるの…

Coqでプログラムや証明を書いたら、そのソースコードを人に見せたりしたくなるときがある。 そのときに便利なcoqdocという機能がある。coqdocはcoqtopやcoqcなどと一緒のところにある。 使いかたは以下。 $ coqdoc [Coqファイル.v] ここで、(** コメント *)…