@[inline]

def Data.DataBool.bool {α : Sort u_1} (ifFalse ifTrue : α) : Bool → α

Case analysis on Bool as a function.

$$\text{bool}(x, y, b) = \begin{cases} x & \text{if } b = \text{false} \\ y & \text{if } b = \text{true} \end{cases}$$

This is the Church encoding eliminator for Bool.

Equations

• Data.DataBool.bool ifFalse ifTrue false = ifFalse
• Data.DataBool.bool ifFalse ifTrue true = ifTrue

@[inline]

def Data.DataBool.guard' {α : Type u_1} (b : Bool) (x : α) : List α

Guard: returns [x] if condition is true, [] otherwise.

$$\text{guard'}(b, x) = \begin{cases} [x] & \text{if } b \\ [] & \text{otherwise} \end{cases}$$

Equations

• Data.DataBool.guard' b x = if b = true then [x] else []

theorem Data.DataBool.bool_false {α : Sort u_1} (x y : α) : bool x y false = x

bool on false returns the first argument.

theorem Data.DataBool.bool_true {α : Sort u_1} (x y : α) : bool x y true = y

bool on true returns the second argument.

theorem Data.DataBool.guard'_true {α : Type u_1} (x : α) : guard' true x = [x]

Guard on true returns a singleton list.

theorem Data.DataBool.guard'_false {α : Type u_1} (x : α) : guard' false x = []

Guard on false returns the empty list.

theorem Data.DataBool.bool_ite {α : Sort u_1} (x y : α) (b : Bool) : bool x y b = if b = true then y else x

bool is the unique function satisfying both bool_false and bool_true.