From ffc9524e6726b109b01441ef46f04a2a6fddfaf9 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 20 Oct 2024 13:29:06 +0900 Subject: [PATCH] =?UTF-8?q?`Type`=20=E3=82=92=E5=9E=8B=E5=85=A8=E4=BD=93?= =?UTF-8?q?=E3=81=A8=E3=81=97=E3=81=A6=E7=B4=B9=E4=BB=8B=E3=81=97=E3=81=AA?= =?UTF-8?q?=E3=81=84?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Type/Type.lean | 2 +- booksrc/SUMMARY.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanByExample/Reference/Type/Type.lean b/LeanByExample/Reference/Type/Type.lean index 5555d32c..b9dd50fe 100644 --- 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 index 0dc78e47..e9b3e325 100644 --- 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)