Skip to content

Commit

Permalink
Update CONTRIBUTING.md
Browse files Browse the repository at this point in the history
句読点についての決まりを追加
  • Loading branch information
Seasawher authored Sep 21, 2023
1 parent 5ffd479 commit 5e5ec6c
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion CONTRIBUTING.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
# CONTRIBUTING

* 句読点は `,` `.` を使用します.
* 地の分の文体は敬体とします.コード例の中のコメントは常体です.
* タクティク `tactic` に対して,記事の名前は `tactic: (日本語による一言説明)` とします.
* `src/SUMMARY.md` のタクティク記事は,アルファベット昇順に並べてください.VSCode だと `Tyriar.sort-lines` という拡張機能があって,並び替えを自動で行うことができます.
* 使用例として紹介する Lean コードは,コンパイルが通るものに関しては `Examples` 配下に配置します.コンパイルが通らないものは,`.md` ファイルの中にコードブロックとして記述します.
* Lean コードの中で `Mathlib``Std` 等のライブラリが必要になった際は,できるだけインポートする範囲を狭めて,必要なものだけインポートするようにしてください.それにより,どのタクティクがどのライブラリに依存しているのかが明確になります.また,動作も軽くなります.たとえば `ring` タクティクを使いたいときは,`import Mathlib.Tactic` ではなくて `import Mathlib.Tactic.Ring` とします.
* `Mathlib``Std` 等のライブラリに依存する例を紹介する際には,それを明記します.
* `Mathlib``Std` 等のライブラリに依存する例を紹介する際には,それを明記します.

0 comments on commit 5e5ec6c

Please sign in to comment.