Merge pull request #936 from lean-ja/Seasawher/issue930

「帰納型」や「構造体」もリンクにする

Examples/Attribute/CasesEliminator.lean

@@ -2,7 +2,7 @@
 
 `[cases_eliminator]` 属性は、[`cases`](../Tactic/Cases.md) タクティクで場合分けをした際の枝を変更します。
 
-より詳しくいうと、[`cases`](../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[cases_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
+より詳しくいうと、[`cases`](../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、[帰納型](../Declarative/Inductive.md) `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[cases_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
 -/
 namespace CasesEliminator --#
 

Examples/Attribute/InductionEliminator.lean

@@ -2,7 +2,7 @@
 
 `[induction_eliminator]` 属性は、帰納法の枝を変更することを可能にします。
 
-より詳しくいうと、[`induction`](../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[induction_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
+より詳しくいうと、[`induction`](../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、[帰納型](../Declarative/Inductive.md) `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[induction_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
 -/
 namespace InductionEliminator --#
 

Examples/Attribute/Simps.lean

@@ -2,7 +2,7 @@
 
 補題を [`simp`](../Tactic/Simp.md) で使えるようにするのは `[simp]` 属性を付与することで可能ですが、`[simps]` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
 
-例えば、ユーザが `Point` という構造体を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
+例えば、ユーザが `Point` という[構造体](../Declarative/Structure.md)を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
 -/
 import Mathlib.Tactic.Simps.Basic -- [simps] 属性を使うため
 

Examples/Declarative/AddAesopRules.lean

@@ -131,7 +131,7 @@ example (a b c d e : Nat)
   aesop
 end --#
 /- ### constructors
-`constructors` ビルダーは、帰納型 `T` の形をしたゴールに遭遇した際に、コンストラクタを適用するように指示します。
+`constructors` ビルダーは、[帰納型](../Declarative/Inductive.md) `T` の形をしたゴールに遭遇した際に、コンストラクタを適用するように指示します。
 -/
 
 /-- 自前で定義した偶数を表す命題 -/

Examples/Declarative/Axiom.lean

@@ -88,7 +88,7 @@ r a b → Quot.mk r a = Quot.mk r b
 * 関数の商へのリフト `Quot.lift`
 * 商の公理 `Quot.sound`
 
-はいずれも他の型からは独立したオブジェクトですが、`Quot.sound` だけが「公理」と呼ばれ、特別扱いされているのは何故でしょうか。以下のように商の公理以外の部分を Lean の帰納型を使って構成してみると理解できるかもしれません。
+はいずれも他の型からは独立したオブジェクトですが、`Quot.sound` だけが「公理」と呼ばれ、特別扱いされているのは何故でしょうか。以下のように商の公理以外の部分を Lean の[帰納型](../Declarative/Inductive.md)を使って構成してみると理解できるかもしれません。
 -/
 
 /-- 標準ライブラリの Quot を真似して自作した型 -/

Examples/Declarative/Class.lean

@@ -43,7 +43,7 @@ instance {α : Type} : Monoid (List α) where
 
 /- ## 型クラス解決
 
-型クラスが行っていることを `class` を使わずにDIYしてみると、型クラスの理解が深まるでしょう。`class` として上で定義したものを、もう一度 [`structure`](./Structure.md) として定義してみます。-/
+型クラスが行っていることを `class` を使わずにDIYしてみると、型クラスの理解が深まるでしょう。`class` として上で定義したものを、もう一度 [構造体](./Structure.md)として定義してみます。-/
 
 /-- 構造体でモノイドクラスを真似たもの -/
 structure Monoid' (α : Type) where
@@ -127,7 +127,7 @@ instance : Plus Nat (List Nat) (List Nat) where
 
 end Good --#
 /- ## class inductive { #ClassInductive }
-基本的に型クラスの下部構造は構造体ですが、一般の帰納型を型クラスにすることも可能です。それには `class inductive` というコマンドを使います。
+基本的に型クラスの下部構造は構造体ですが、一般の[帰納型](../Declarative/Inductive.md)を型クラスにすることも可能です。それには `class inductive` というコマンドを使います。
 -/
 
 /-- 全単射があるという同値関係 -/

Examples/Declarative/Structure.lean

@@ -81,7 +81,7 @@ def foo' : Nat × (Int × String) := ⟨1, 2, "foo"⟩
 
 #guard foo = foo'
 
-/- 一般の帰納型に対しては使用できません。-/
+/- 一般の[帰納型](../Declarative/Inductive.md)に対しては使用できません。-/
 
 inductive Sample where
   | fst (foo bar : Nat) : Sample

Examples/Diagnostic/Whnf.lean

@@ -1,7 +1,7 @@
 /- # \#whnf
 `#whnf` は、式を弱頭正規形(weak head normal form)に簡約するコマンドです。
 
-弱頭正規形とは、式の構成要素の最初の部分(head)がそれ以上簡約できない形になっている状態のことです。たとえば式の頭が帰納型のコンストラクタや、ラムダ式になっていれば弱頭正規形です。
+弱頭正規形とは、式の構成要素の最初の部分(head)がそれ以上簡約できない形になっている状態のことです。たとえば式の頭が[帰納型](../Declarative/Inductive.md)のコンストラクタや、ラムダ式になっていれば弱頭正規形です。
 -/
 import Mathlib.Tactic.Conv -- `#whnf` コマンドを使うために必要
 

Examples/Tactic/Cases.lean

@@ -43,7 +43,7 @@ example : P ∨ Q → (P → R) → (Q → R) → R := by
 
 /- ## 舞台裏
 
-`cases` は、実際には論理和に限らず帰納型をコンストラクタに分解することができるタクティクです。
+`cases` は、実際には論理和に限らず[帰納型](../Declarative/Inductive.md)をコンストラクタに分解することができるタクティクです。
 論理和を分解することができるのも、`Or` が帰納型として定義されているからです。
 -/
 namespace Cases --#

Examples/Tactic/Constructor.lean

@@ -45,7 +45,7 @@ example (h : P ↔ Q) (hP : P) : Q := by
   apply pq
   assumption
 
-/- また論理積や同値性は構造体なので、次の関数も利用できます。-/
+/- また論理積や同値性は[構造体](../Declarative/Structure.md)なので、次の関数も利用できます。-/
 
 -- 論理積から構成要素を取り出す関数
 #check (And.left : P ∧ Q → P)

Examples/Tactic/Exact.lean

@@ -16,10 +16,10 @@ example (hP : P) (hQ : Q) : P ∧ Q := by
 
 example (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ
 
-/-! なお `And` は構造体なので[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/
+/- なお `And` は[構造体](../Declarative/Structure.md)なので[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)記法を用いて次のように書くこともできます。-/
 
 example (hP : P) (hQ : Q) : P ∧ Q := ⟨hP, hQ⟩
 
-/-! ## assumption との関連
+/- ## assumption との関連
 
 `exact` は常にどの命題を使うか明示する必要がありますが、「ゴールを `exact` で閉じることができるような命題をローカルコンテキストから自動で探す」 [`assumption`](./Assumption.md) というタクティクもあります。-/

Examples/Tactic/Exfalso.lean

@@ -19,7 +19,7 @@ example (h : P) (hn : ¬ P) : P ∧ Q := by
 /- ローカルコンテキスト内に `P` と `¬ P` があって矛盾することを指摘したい場合は、[`contradiction`](./Contradiction.md) を使うとより簡潔です。また、一般に問題が命題論理に帰着されている状況では [`tauto`](./Tauto.md) または [`itauto`](./Itauto.md) が利用できます。-/
 
 /- ## 舞台裏
-矛盾つまり `False` の項からはどんな命題でも示せるというのは最初は奇妙に感じるかもしれません。実際に `False` の構成を真似て自分で帰納型を定義することによって、同様のことを再現できます。
+矛盾つまり `False` の項からはどんな命題でも示せるというのは最初は奇妙に感じるかもしれません。実際に `False` の構成を真似て自分で[帰納型](../Declarative/Inductive.md)を定義することによって、同様のことを再現できます。
 -/
 
 universe u

Examples/Tactic/Exists.lean

@@ -27,7 +27,7 @@ Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
 -- このとき `w : α` と `h : p w` が与えられたとき `∃ x : α, p x` が成り立つ。
 #check (Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α) (h : p w), Exists p)
 
-/- したがって `Exists` は単一のコンストラクタを持つ帰納型、つまり構造体なので、上記の `exists` は `exact` と[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
+/- したがって `Exists` は単一のコンストラクタを持つ[帰納型](../Declarative/Inductive.md)、つまり[構造体](../Declarative/Structure.md)なので、上記の `exists` は `exact` と[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)で次のように書き直すことができます。-/
 
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exact ⟨2, show 3 * 2 + 1 = 7 from by rfl⟩

Examples/Tactic/Ext.lean

@@ -27,7 +27,7 @@ example : s ∩ t = t ∩ s := by
   aesop
 
 /- ## [ext] 属性
-`[ext]` 属性を命題に与えると、上記のようにその命題は `ext` タクティクで利用できるようになります。さらに、`[ext]` 属性は構造体に対しても与えることができます。このとき、その構造体に対して自動的に `.ext` と `.ext_iff` の２つの定理が生成されます。
+`[ext]` 属性を命題に与えると、上記のようにその命題は `ext` タクティクで利用できるようになります。さらに、`[ext]` 属性は[構造体](../Declarative/Structure.md)に対しても与えることができます。このとき、その構造体に対して自動的に `.ext` と `.ext_iff` の２つの定理が生成されます。
 -/
 
 variable {α : Type}

Examples/Tactic/Have.lean

@@ -21,11 +21,11 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
 
 また `have` で同じ名前を2回宣言すると、古い方はアクセス不能になってしまいます。ローカルコンテキストの補題の置き換えを行いたいときは、代わりに `replace` を使用してください。 -/
 
-/-! ## 無名コンストラクタ
+/- ## 無名コンストラクタ
 
 `P` の証明 `hp : P` と `Q` の証明 `hq : Q` があるとき、`P ∧ Q` の証明は `And.intro hp hq` で構成できます。ここで `And.intro` は構造体 `And` 型のコンストラクタです。
 
-これを、コンストラクタ名を明示せずにシンプルに `⟨hp, hq⟩` と書くことができます。これは[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)と呼ばれるもので、`And` に限らず任意の構造体に使用することができます。-/
+これを、コンストラクタ名を明示せずにシンプルに `⟨hp, hq⟩` と書くことができます。これは[無名コンストラクタ](../Declarative/Structure.md#AnonymousConstructor)と呼ばれるもので、`And` に限らず任意の[構造体](../Declarative/Structure.md)に使用することができます。-/
 variable (hp : P) (hq : Q)
 
 def hpq : P ∧ Q := ⟨hp, hq⟩

Examples/Tactic/Obtain.lean

@@ -29,7 +29,7 @@ example (h : ∃ e : X, P e) : True := by
   trivial
 
 /-
-`obtain` に与えることのできるパターンは [`rcases`](./Rcases.md) に与えられるパターンと同様で、一般の帰納型を分解することができます。
+`obtain` に与えることのできるパターンは [`rcases`](./Rcases.md) に与えられるパターンと同様で、一般の[帰納型](../Declarative/Inductive.md)を分解することができます。
 -/
 
 inductive Sample where

Examples/Tactic/Rcases.lean

@@ -23,7 +23,7 @@ example : P ∧ Q → Q ∧ P := by
   -- `Q ∧ P` を証明する
   exact ⟨hQ, hP⟩
 
-/- `rcases` は一般には `⟨x₁, x₂, ...⟩ | ⟨y₁, y₂, ...⟩ | ...` という記法で帰納型の分解が可能です。-/
+/- `rcases` は一般には `⟨x₁, x₂, ...⟩ | ⟨y₁, y₂, ...⟩ | ...` という記法で[帰納型](../Declarative/Inductive.md)の分解が可能です。-/
 
 inductive Sample where
   | foo (x y : Nat) : Sample

Examples/Type/Prop.lean

@@ -21,7 +21,7 @@
 #guard (False ∧ True) = False
 #guard (False ∧ False) = False
 
-/- Lean では `And` という名前の構造体(structure)として表現されます。-/
+/- Lean では `And` という名前の[構造体](../Declarative/Structure.md)として表現されます。-/
 
 example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ
 
@@ -34,7 +34,7 @@ example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := And.intro hP hQ
 #guard False ∨ True
 #guard (False ∨ False) = False
 
-/- Lean では `Or` という名前の帰納型(inductive type)として表現されます。-/
+/- Lean では `Or` という名前の[帰納型](../Declarative/Inductive.md)として表現されます。-/
 
 example (P Q : Prop) (hP : P) : P ∨ Q := Or.inl hP
 

Examples/TypeClass/Decidable.lean

@@ -44,7 +44,7 @@ instance (n : Nat) : Decidable (Even n) := by
 example : Even 4 := by decide
 
 /- ## class inductive
-`Decidable` 型クラスの定義は少し特殊です。コンストラクタが複数あり、構造体ではなく帰納型の構造をしています。これは `Decidable` が [`class inductive`](../Declarative/Class.md#ClassInductive) というコマンドで定義されているためです。-/
+`Decidable` 型クラスの定義は少し特殊です。コンストラクタが複数あり、[構造体](../Declarative/Structure.md)ではなく[帰納型](../Declarative/Inductive.md)の構造をしています。これは `Decidable` が [`class inductive`](../Declarative/Class.md#ClassInductive) というコマンドで定義されているためです。-/
 
 /--
 info: inductive Decidable : Prop → Type

Examples/TypeClass/Repr.lean

@@ -2,7 +2,7 @@
 # Repr
 `Repr` は、その型の項をどのように表示するかを指示する型クラスです。
 
-たとえば、以下のように新しく構造体 `Point` を定義したとき、特に何も指定しなければ `Point` の項を `#eval` で表示することはできません。
+たとえば、以下のように新しく[構造体](../Declarative/Structure.md) `Point` を定義したとき、特に何も指定しなければ `Point` の項を `#eval` で表示することはできません。
 -/
 namespace Repr --#