Type を型全体として紹介しない

lean-ja · Oct 20, 2024 · ffc9524 · ffc9524
1 parent 22cb886
commit ffc9524
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/LeanByExample/Reference/Type/Type.lean b/LeanByExample/Reference/Type/Type.lean
@@ -1,5 +1,5 @@
 /- # Type
-`Type` は、型全体がなす型宇宙です。ここで型宇宙とは、項が再び型であるような型のことをいいます。
+`Type` は、型がなす型宇宙です。ここで型宇宙とは、項が再び型であるような型のことをいいます。
 
 たとえば `Nat` や `Int`, `Bool` や `String` などが `Type` の項になっています。
 -/

diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
@@ -96,7 +96,7 @@
   - [List: 連結リスト](./Reference/Type/List.md)
   - [Prop: 命題全体](./Reference/Type/Prop.md)
   - [String: 文字列](./Reference/Type/String.md)
-  - [Type: 型全体](./Reference/Type/Type.md)
+  - [Type: 型の型](./Reference/Type/Type.md)
 
 - [タクティク](./Reference/Tactic/README.md)
   - [<;> 生成された全ゴールに適用](./Reference/Tactic/SeqFocus.md)