CONTRIBUTING 更新 - 誤解を招く記述を修正するなど

CONTRIBUTING.md

@@ -5,11 +5,13 @@
 * 句読点は `,` `.` を使用します．
 * 地の分の文体は敬体とします．コード例の中のコメントは常体です．
 * タクティク `tactic` に対して，記事の名前は `tactic: (日本語による一言説明)` とします．
-* `src/SUMMARY.md` のタクティク記事は，アルファベット昇順に並べてください．VSCode だと `Tyriar.sort-lines` という拡張機能があって，並び替えを自動で行うことができます．
+* `src/SUMMARY.md` のタクティク記事は，アルファベット昇順に並べてください．VSCode だと `Tyriar.sort-lines` という拡張機能があって，並び替えを自動で行うことができます．`Examples.lean` についても同様です．
 
 ## コード例
 
-* 使用例として紹介する Lean コードは，コンパイルが通るようにして `Examples` 配下に配置します．「タクティクが失敗する例」を紹介したいときであっても `try` を使ってコンパイルが通るようにしてください．
-* 新しいタクティクのコード例を追加したら，`Examples.lean` ファイルに追記してください．
+* 使用例として紹介する Lean コードは，コンパイルが通るようにして `Examples` 配下に配置します．「タクティクが失敗する例」を紹介したいときであっても `try` を使ってコンパイルが通るようにしてください．コード例が正しいかチェックする際にその方が楽だからです．
+* `Examples` ディレクトリにファイル `TacticName.lean` を新たに追加するときは，`src` ディレクトリにも `tactic_name.md` ファイルを追加してください．
+* `Examples` ディレクトリに新しいファイルを追加したら，`Examples.lean` ファイルに追記してください．これは，CI でコード例が正しいことをテストするためです．
 * Lean コードの中で `Mathlib` や `Std` 等のライブラリが必要になった際は，できるだけインポートする範囲を狭めて，必要なものだけインポートするようにしてください．それにより，どのタクティクがどのライブラリに依存しているのかが明確になります．また，動作も軽くなります．たとえば `ring` タクティクを使いたいときは，`import Mathlib.Tactic` ではなくて `import Mathlib.Tactic.Ring` とします．
 * `Mathlib` や `Std` 等のライブラリに依存する例を紹介する際には，`needs: import ...` という形式でそれを明記します．
+* タクティクの名前の由来についてコメントする際は，`named after:` という形式で書いてください．