9.11. Booleans

inductive type

Bool : Type

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.

Constructors

false : _root_.Bool

The boolean value false, not to be confused with the proposition False.
true : _root_.Bool

The boolean value true, not to be confused with the proposition True.

The constructors Bool.true and Bool.false are exported from the Bool namespace, so they can be written true and false.

9.11.1. Run-Time Representation

Because Bool is an enum inductive type, it is represented by a single byte in compiled code.

9.11.2. Booleans and Propositions

Both Bool and Prop represent notions of truth. From a purely logical perspective, they are equivalent: propositional extensionality means that there are fundamentally only two propositions, namely True and False. However, there is an important pragmatic difference: Bool classifies values that can be computed by programs, while Prop classifies statements for which code generation doesn't make sense. In other words, Bool is the notion of truth and falsehood that's appropriate for programs, while Prop is the notion that's appropriate for mathematics. Because proofs are erased from compiled programs, keeping Bool and Prop distinct makes it clear which parts of a Lean file are intended for computation.

A Bool can be used wherever a Prop is expected. There is a coercion from every Bool b to the proposition b = true. By propext, true = true is equal to True, and false = true is equal to False.

Not every proposition can be used by programs to make run-time decisions. Otherwise, a program could branch on whether the Collatz conjecture is true or false! Many propositions, however, can be checked algorithmically. These propositions are called decidable propositions, and have instances of the Decidable type class. The function Decidable.decide converts a proof-carrying Decidable result into a Bool. This function is also a coercion from decidable propositions to Bool, so (2 = 2 : Bool) evaluates to true.

9.11.3. Syntax

syntax

The infix operators &&, ||, and ^^ are notations for Bool.and, Bool.or, and Bool.xor, respectively.

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 && term

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 || term

term ::= ...
    | Boolean exclusive or term ^^ term

syntax

The prefix operator ! is notation for 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).
!term

9.11.4. API Reference

9.11.4.1. Logical Operations

The functions cond, and, and or are short-circuiting. In other words, false && BIG_EXPENSIVE_COMPUTATION does not need to execute BIG_EXPENSIVE_COMPUTATION before returning false. These functions are defined using the macro_inline attribute, which causes the compiler to replace calls to them with their definitions while generating code, and the definitions use nested pattern matching to achieve the short-circuiting behavior.

def

cond.{u} {α : Type u} (c : Bool) (x y : α) : α

cond b x y is the same as if b then x else y, but optimized for a boolean condition. It can also be written as bif b then x else y. This is @[macro_inline] because x and y should not be eagerly evaluated (see ite).

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.

def

Bool.or (x y : Bool) : Bool

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.

def

Bool.xor : Bool → Bool → Bool

Boolean exclusive or

def

Bool.atLeastTwo (a b c : Bool) : Bool

At least two out of three booleans are true.

9.11.4.2. Comparisons

def

Bool.decEq (a b : Bool) : Decidable (a = b)

Decidable equality for Bool

9.11.4.3. Conversions

def

Bool.toISize (b : Bool) : ISize

def

Bool.toUInt8 (b : Bool) : UInt8

def

Bool.toUInt16 (b : Bool) : UInt16

def

Bool.toUInt32 (b : Bool) : UInt32

def

Bool.toUInt64 (b : Bool) : UInt64

def

Bool.toUSize (b : Bool) : USize

def

Bool.toInt8 (b : Bool) : Int8

def

Bool.toInt16 (b : Bool) : Int16

def

Bool.toInt32 (b : Bool) : Int32

def

Bool.toInt64 (b : Bool) : Int64

def

Bool.toNat (b : Bool) : Nat

convert a Bool to a Nat, false -> 0, true -> 1