Merge pull request #1051 from lean-ja/Seasawher/issue505

Bool を紹介する

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` になるため計算可能であるという含みがあります。-/

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)