Bool is the type of boolean values, true and false. Classically,
this is equivalent to Prop (the type of propositions), but the distinction
is important for programming, because values of type Prop are erased in the
code generator, while Bool corresponds to the type called bool or boolean
in most programming languages.
12.11. 真偽値（Booleans）
inductive type
Bool : Type
コンストラクタ Bool.true と Bool.false は Bool 名前空間からエクスポートされるため、 true と false と書くことができます。
12.11.1. ランタイム表現（Run-Time Representation）
12.11.2. 真偽値と命題（Booleans and Propositions）
Bool と Prop はどちらも真理の概念を表します。純粋論理の観点から見ると、両者は同等です： propositional extensionality は基本的に2つの命題、すなわち True と False しか存在しないことを意味します。しかし、実用上は重要な違いがあります： Bool はプログラムで計算できる 値 を分類し、 Prop はコード生成が意味を為さない文を分類します。言い換えると、 Bool はプログラムに適した真偽の概念であり、 Prop は数学に適した概念です。コンパイルされたプログラムから証明は消去されるため、 Bool と Prop を区別しておくことで Lean ファイルのどの部分が計算を目的としているかが明確になります。
Bool は Prop が期待されているところではどこでも使うことができます。すべての Bool b から命題 b = true への coercion が存在します。 propext により、 true = true は True に、 false = true は False にそれぞれ等しいです。
全ての命題をプログラムがランタイム時の判断に使えるわけではありません。そうでなければコラッツ予想が真か偽かでプログラムが分岐してしまいます！しかし、多くの命題はアルゴリズムでチェックすることができます。これらの命題は 決定可能 な命題と呼ばれ、 Decidable 型クラスを持ちます。関数 Decidable.decide は証明を格納した Decidable の結果を Bool に変換します。この関数は決定可能な命題から Bool への強制演算でもあるため、 (2 = 2 : Bool) は true と評価されます。
12.11.3. 構文（Syntax）
syntax
中置演算子 && ・ || ・ ^^ はそれぞれ Bool.and ・ Bool.or ・ Bool.xor の表記です。
term ::= ...
| `and x y`, or `x && y`, is the boolean "and" operation (not to be confused
with `And : Prop → Prop → Prop`, which is the propositional connective).
It is `@[macro_inline]` because it has C-like short-circuiting behavior:
if `x` is false then `y` is not evaluated.
term ::= ...
| `or x y`, or `x || y`, is the boolean "or" operation (not to be confused
with `Or : Prop → Prop → Prop`, which is the propositional connective).
It is `@[macro_inline]` because it has C-like short-circuiting behavior:
if `x` is true then `y` is not evaluated.
term ::= ...
| Boolean exclusive or
syntax
前置演算子 ! は Bool.not の表記です。
term ::= ...
| `not x`, or `!x`, is the boolean "not" operation (not to be confused
with `Not : Prop → Prop`, which is the propositional connective).
12.11.4. API リファレンス（API Reference）
12.11.4.1. 論理演算子（Logical Operations）
関数 cond ・ and ・ or は短絡します。つまり、 false && BIG_EXPENSIVE_COMPUTATION は false を返す前に BIG_EXPENSIVE_COMPUTATION を実行する必要はありません。これらの関数は macro_inline 属性を使用して定義されています。これによりコンパイラはコードを生成する際に関数の呼び出しを定義に置き換え、入れ子のパターンマッチを用いる定義が短絡評価されるようになります。
def
cond.{u} {α : Type u} (c : Bool) (x y : α) : α
def
Bool.not : Bool → Bool
not x, or !x, is the boolean "not" operation (not to be confused
with Not : Prop → Prop, which is the propositional connective).
def
Bool.and (x y : Bool) : Bool
and x y, or x && y, is the boolean "and" operation (not to be confused
with And : Prop → Prop → Prop, which is the propositional connective).
It is @[macro_inline] because it has C-like short-circuiting behavior:
if x is false then y is not evaluated.