From 8dc8eb51b48ac3b532a4d9447a3c88a06671d6f5 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 4 Nov 2024 17:23:46 +0900
Subject: [PATCH] =?UTF-8?q?Bool=20=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99?=
 =?UTF-8?q?=E3=82=8B=20Fixes=20#505?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Type/Bool.lean | 19 +++++++++++++++++++
 booksrc/SUMMARY.md                     |  1 +
 2 files changed, 20 insertions(+)
 create mode 100644 LeanByExample/Reference/Type/Bool.lean

diff --git a/LeanByExample/Reference/Type/Bool.lean b/LeanByExample/Reference/Type/Bool.lean
new file mode 100644
index 0000000..41592fe
--- /dev/null
+++ b/LeanByExample/Reference/Type/Bool.lean
@@ -0,0 +1,19 @@
+/- # Bool
+
+`Bool` は真偽値を表す型です。`true` と `false` の２つの値を持ちます。
+-/
+
+#check (true : Bool)
+#check (false : Bool)
+
+/- `Bool` の値を得るためには、たとえば `==` を用いて値を比較します。-/
+
+inductive Foo where
+  | bar
+  | baz
+  deriving BEq
+
+example : Bool := Foo.bar == Foo.bar
+example : Bool := Foo.bar != Foo.baz
+
+/- 真偽を表すという点で [`Prop`](./Prop.md) と似ていますが、`Bool` の項は簡約すれば必ず `true` か `false` になるため計算可能であるという含みがあります。-/
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index b530400..7d8235b 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -91,6 +91,7 @@
   - [ToString: 文字列に変換](./Reference/TypeClass/ToString.md)
 
 - [型](./Reference/Type/README.md)
+  - [Bool: 真偽値](./Reference/Type/Bool.md)
   - [Char: Unicode 文字](./Reference/Type/Char.md)
   - [Float: 浮動小数点数](./Reference/Type/Float.md)
   - [List: 連結リスト](./Reference/Type/List.md)