9.9. 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.

Planned Content
  • Relationship to Prop

  • Laziness of && etc

Tracked at issue #162