From 140f64b664bcfc253b69550260ae30bb2afcbc95 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 23 Sep 2023 14:13:18 +0900 Subject: [PATCH] =?UTF-8?q?markdown=20=E3=83=95=E3=82=A1=E3=82=A4=E3=83=AB?= =?UTF-8?q?=E3=81=AB=E3=82=B3=E3=83=BC=E3=83=89=E4=BE=8B=E3=82=92=E7=9B=B4?= =?UTF-8?q?=E6=8E=A5=E6=9B=B8=E3=81=8B=E3=81=AA=E3=81=84=E3=82=88=E3=81=86?= =?UTF-8?q?=E3=81=AB=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CONTRIBUTING.md | 10 ++++++++-- Examples/Induction.lean | 9 +++++++++ src/apply.md | 10 ---------- src/induction.md | 4 +--- 4 files changed, 18 insertions(+), 15 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 6e7b6ea0..2d2a8058 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,9 +1,15 @@ # CONTRIBUTING +## 文体など + * 句読点は `,` `.` を使用します． * 地の分の文体は敬体とします．コード例の中のコメントは常体です． * タクティク `tactic` に対して，記事の名前は `tactic: (日本語による一言説明)` とします． * `src/SUMMARY.md` のタクティク記事は，アルファベット昇順に並べてください．VSCode だと `Tyriar.sort-lines` という拡張機能があって，並び替えを自動で行うことができます． -* 使用例として紹介する Lean コードは，コンパイルが通るものに関しては `Examples` 配下に配置します．コンパイルが通らないものは，`.md` ファイルの中にコードブロックとして記述します． + +## コード例 + +* 使用例として紹介する Lean コードは，コンパイルが通るようにして `Examples` 配下に配置します．「タクティクが失敗する例」を紹介したいときであっても `try` を使ってコンパイルが通るようにしてください． +* 新しいタクティクのコード例を追加したら，`Examples.lean` ファイルに追記してください． * Lean コードの中で `Mathlib` や `Std` 等のライブラリが必要になった際は，できるだけインポートする範囲を狭めて，必要なものだけインポートするようにしてください．それにより，どのタクティクがどのライブラリに依存しているのかが明確になります．また，動作も軽くなります．たとえば `ring` タクティクを使いたいときは，`import Mathlib.Tactic` ではなくて `import Mathlib.Tactic.Ring` とします． -* `Mathlib` や `Std` 等のライブラリに依存する例を紹介する際には，それを明記します． +* `Mathlib` や `Std` 等のライブラリに依存する例を紹介する際には，`needs: import ...` という形式でそれを明記します． diff --git a/Examples/Induction.lean b/Examples/Induction.lean index a3566f7e..ed62ebd6 100644 --- a/Examples/Induction.lean +++ b/Examples/Induction.lean @@ -3,6 +3,15 @@ import Mathlib.Tactic.Cases import Mathlib.Tactic.Positivity +namespace Examples + +-- ANCHOR: nat +inductive Nat + | zero : Nat + | succ (n : Nat) : Nat +-- ANCHOR_END: nat + +end Examples -- ANCHOR: first -- 階乗関数 diff --git a/src/apply.md b/src/apply.md index 4ea4fb0c..f7382ae8 100644 --- a/src/apply.md +++ b/src/apply.md @@ -26,16 +26,6 @@ `apply` には引数が必須なのですが，省略しても近くにエラーが出ません．一般に，構文的に間違った証明を書いた場合には，エラーがわかりやすい場所に出てくれる保証はありません． -```lean -example (h: P → Q) : ¬Q → ¬P := by - -- 引数は必須なので間違っているが，エラーが近くに出ない - apply - --- ここにエラーが出る -example (hP: P) : P := by - exact hP -``` - ## 関連するタクティク ### [exact](./exact.md) diff --git a/src/induction.md b/src/induction.md index 29541b4b..3d08bdbb 100644 --- a/src/induction.md +++ b/src/induction.md @@ -5,9 +5,7 @@ 自然数を例に説明します．Lean では自然数は次のように帰納的に定義されています. ```lean -inductive Nat - | zero : Nat - | succ (n : Nat) : Nat +{{#include ../Examples/Induction.lean:nat}} ``` `succ` は後者関数と呼ばれる関数で，`n + 1 := succ n` です．