@[reducible, inline]

abbrev Data.Void : Type

The void type $\bot$ — uninhabited. Wraps Lean's Empty.

There exist no values of type $\text{Void}$, so any function $\text{Void} \to \alpha$ is vacuously total.

Equations

• Data.Void = Empty

def Data.Void.absurd {α : Sort u} (v : Void) : α

Eliminate from $\bot$ to any type: given $v : \bot$, produce any $\alpha$.

$$\text{absurd} : \bot \to \alpha$$

This is the ex falso quodlibet principle.

Equations

• v.absurd = Empty.elim v

@[implicit_reducible]

instance Data.Void.instBEq : BEq Void

BEq instance for $\bot$. Vacuously satisfied since no two values exist to compare.

Equations

• Data.Void.instBEq = { beq := fun (v x : Data.Void) => v.absurd }

@[implicit_reducible]

instance Data.Void.instOrd : Ord Void

Ord instance for $\bot$. Vacuously satisfied since no values exist to order.

Equations

• Data.Void.instOrd = { compare := fun (v x : Data.Void) => v.absurd }

@[implicit_reducible]

instance Data.Void.instToString : ToString Void

ToString instance for $\bot$. Vacuously satisfied — no value can be stringified.

Equations

• Data.Void.instToString = { toString := fun (v : Data.Void) => v.absurd }

@[implicit_reducible]

instance Data.Void.instRepr : Repr Void

Repr instance for $\bot$. Vacuously satisfied.

Equations

• Data.Void.instRepr = { reprPrec := fun (v : Data.Void) (x : Nat) => v.absurd }

@[implicit_reducible]

instance Data.Void.instHashable : Hashable Void

Hashable instance for $\bot$. Vacuously satisfied.

Equations

• Data.Void.instHashable = { hash := fun (v : Data.Void) => v.absurd }

@[implicit_reducible]

instance Data.Void.instInhabitedForall {α : Sort u_1} : Inhabited (Void → α)

The function space $\bot \to \alpha$ is inhabited, witnessed by absurd.

Since $|\bot| = 0$, there is exactly one function $\bot \to \alpha$ for any $\alpha$.

Equations

• Data.Void.instInhabitedForall = { default := Data.Void.absurd }

theorem Data.Void.eq_absurd {α : Sort u_1} (f : Void → α) : f = absurd

Any function from $\bot$ is vacuously equal to absurd:

$$\forall\, f : \bot \to \alpha,\; f = \text{absurd}$$

This follows because the function space $\bot \to \alpha$ is a singleton.