Coqで依存型 - にわとり小屋でのプログラミング
最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるのだ。 Variable A:Set. Inductive Vec : nat -> Set := | VNil : Vec O | VCons : forall n, A -> Vec n -> Vec (S n). このベクトル型を使えば、コンパイル時に長さの整合性もチェックしてくれて、間違いがある場所を教えてくれる。コンパイルさえ通れば、OutOfBoundsExceptionのような実行時エラーは起こりえないことが保証される。 例えば、一般的にリストのhead関数は、引数が1以上の長さのときのみ定義でき、空リストの場合には値
Gallina の構文と Vernacular コマンド
Gallina の構文と Vernacular コマンド 字句 空白文字、改行、タブは空白とみなされる。 コメントは (* で始まり *) で終わる。コメントの中に他のコメントあるいは文字列を入れることができる。コメントは空白とみなされる。 識別子には、英字 (A, B, …)、下線 (_) その他 Unicode で識別子として利用可能とされている文字が使える。識別子の二文字目以降には数字およびプライム (') も使える。 キーワード 特殊な意味を持つため識別子として使えないキーワードは以下の通り: _ as at cofix else end exists exists2 fix for forall fun if IF in let match mod Prop return Set then Type using where with 項 全称量化子 forall n, 0 fo
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
