Coqコーディング規約
全般
- コンパイルできないコードはコミットしない
- 使用しているCoqのバージョンをREADMEに書く
タクティックに関すること
- bulletを使う (https://coq.inria.fr/refman/Reference-Manual009.html#sec332)
- 同じ時点でできたサブゴールは、同じインデントにする
- サブゴールの末尾はterminatorまたはnowタクティカルを使う
- 新しく生成される変数名、仮定の名前を明示する
- 例: introsタクティックでは引数を明示し、数と名前を指定
- 例: destructタクティックではasで新しくできる変数名を明示
- optional(セミコロンは前半のタクティックでサブゴールが増える場合以外は使わない)
- bulletを使う (https://coq.inria.fr/refman/Reference-Manual009.html#sec332)
- 同じ時点でできたサブゴールは、同じインデントにする
- サブゴールの末尾はterminatorまたはnowタクティカルを使う
- 新しく生成される変数名、仮定の名前を明示する
- 例: introsタクティックでは引数を明示し、数と名前を指定
- 例: destructタクティックではasで新しくできる変数名を明示
- optional(セミコロンは前半のタクティックでサブゴールが増える場合以外は使わない)
Author And Source
この問題について(Coqコーディング規約), 我々は、より多くの情報をここで見つけました https://qiita.com/yoshihiro503/items/730eba53797de7a23328著者帰属：元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .