Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Booleans

The built-in Boolean type has two constructors:

Inductive bool : Set :=
    true : bool | false : bool

Induction principles

Coq automatically defines an induction principle:

Search (∀ b: bool, _ b) "_ind".bool_ind:
  ∀ P : bool → Prop,
    P true → P false → ∀ b : bool, P b