markdown ファイルにコード例を直接書かないようにする

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 ...` という形式でそれを明記します．

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
 -- 階乗関数

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)

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` です．