Merge pull request #840 from lean-ja/Seasawher/issue839

目次の順番の入れ替え

Author: Seasawher

src/SUMMARY.md

@@ -68,6 +68,22 @@
   - [match_pattern: 独自パタンマッチ](./Attribute/MatchPattern.md)
   - [simps: simp補題の自動生成](./Attribute/Simps.md)
 
+- [型クラス](./TypeClass/README.md)
+  - [Coe: 型強制](./TypeClass/Coe.md)
+  - [CoeDep: 依存型強制](./TypeClass/CoeDep.md)
+  - [CoeFun: 関数型への強制](./TypeClass/CoeFun.md)
+  - [CoeSort: 型宇宙への強制](./TypeClass/CoeSort.md)
+  - [Decidable: 決定可能](./TypeClass/Decidable.md)
+  - [GetElem: n番目の要素を取得](./TypeClass/GetElem.md)
+  - [Inhabited: 有項にする](./TypeClass/Inhabited.md)
+  - [OfNat: 数値リテラルを使用](./TypeClass/OfNat.md)
+  - [Repr: 表示方法を指定](./TypeClass/Repr.md)
+  - [ToString: 文字列に変換](./TypeClass/ToString.md)
+
+- [型](./Type/README.md)
+  - [Prop: 命題全体](./Type/Prop.md)
+  - [Type: 型全体](./Type/Type.md)
+
 - [タクティク](./Tactic/README.md)
   - [<;> 生成された全ゴールに適用](./Tactic/SeqFocus.md)
   - [ac_rfl: 可換性と結合性を使う](./Tactic/AcRfl.md)
@@ -150,22 +166,6 @@
   - [with_reducible: 透過度指定](./Tactic/WithReducible.md)
   - [wlog: 一般性を失わずに特殊化](./Tactic/Wlog.md)
 
-- [型クラス](./TypeClass/README.md)
-  - [Coe: 型強制](./TypeClass/Coe.md)
-  - [CoeDep: 依存型強制](./TypeClass/CoeDep.md)
-  - [CoeFun: 関数型への強制](./TypeClass/CoeFun.md)
-  - [CoeSort: 型宇宙への強制](./TypeClass/CoeSort.md)
-  - [Decidable: 決定可能](./TypeClass/Decidable.md)
-  - [GetElem: n番目の要素を取得](./TypeClass/GetElem.md)
-  - [Inhabited: 有項にする](./TypeClass/Inhabited.md)
-  - [OfNat: 数値リテラルを使用](./TypeClass/OfNat.md)
-  - [Repr: 表示方法を指定](./TypeClass/Repr.md)
-  - [ToString: 文字列に変換](./TypeClass/ToString.md)
-
-- [型](./Type/README.md)
-  - [Prop: 命題全体](./Type/Prop.md)
-  - [Type: 型全体](./Type/Type.md)
-
 - [演習問題](./Exercise/README.md)
   - [床屋のパラドクス](./Exercise/BarberParadox.md)
   - [「ならば」の定義を疑う](./Exercise/DoubtImplication.md)