From efcf263f450db5993ff326548e249b2448c97445 Mon Sep 17 00:00:00 2001
From: Kitamado <47292598+Seasawher@users.noreply.github.com>
Date: Thu, 5 Oct 2023 08:01:23 +0900
Subject: [PATCH] =?UTF-8?q?CONTRIBUTING.md=20=E3=82=92=E6=9B=B4=E6=96=B0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CONTRIBUTING.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index f2626233..3bd5db40 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -6,6 +6,8 @@
 * 地の分の文体は敬体とします．コード例の中のコメントは常体です．
 * タクティク `tactic` に対して，記事の名前は `tactic: (日本語による一言説明)` とします．
 * `src/SUMMARY.md` のタクティク記事は，アルファベット昇順に並べてください．VSCode だと `Tyriar.sort-lines` という拡張機能があって，並び替えを自動で行うことができます．`Examples.lean` についても同様です．
+* タクティクの名前の由来についてコメントする際は，`named after:` という形式で書いてください．
+* `Mathlib` や `Std` 等のライブラリに依存するタクティクを紹介する際には，`needs: import ...` という形式でそれを明記します．
 
 ## コード例
 
@@ -13,5 +15,5 @@
 * `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:` という形式で書いてください．
+
+