# Order-related type synonyms #

In this file we define `WithBot`, `WithTop`, `ENat`, and `PNat`. The definitions were moved to this file without any theory so that, e.g., `Data/Countable/Basic` can prove `Countable ENat` without exploding its imports.

source
def WithBot (α : Type u_2) :
Type u_2

Attach `⊥` to a type.

Equations

- WithBot α = Option α

Instances For

source
instance WithBot.instRepr {α : Type u_1} [Repr α] :
Repr (WithBot α)
Equations

- WithBot.instRepr = { reprPrec := fun (o : WithBot α) (x : ℕ) => match o with | none => Std.Format.text "⊥" | some a => Std.Format.text "↑" ++ repr a }

source
@[match_pattern]
def WithBot.some {α : Type u_1} :
α → WithBot α

The canonical map from `α` into `WithBot α`

Equations

- WithBot.some = some

Instances For

source
instance WithBot.coe {α : Type u_1} :
Coe α (WithBot α)
Equations

- WithBot.coe = { coe := WithBot.some }

source
instance WithBot.bot {α : Type u_1} :
Bot (WithBot α)
Equations

- WithBot.bot = { bot := none }

source
instance WithBot.inhabited {α : Type u_1} :
Inhabited (WithBot α)
Equations

- WithBot.inhabited = { default := ⊥ }

source
def WithBot.recBotCoe {α : Type u_1} {C : WithBot α → Sort u_2} (bot : C ⊥) (coe : (a : α) → C ↑a) (n : WithBot α) :
C n

Recursor for `WithBot` using the preferred forms `⊥` and `↑a`.

Equations

- WithBot.recBotCoe bot coe none = bot
- WithBot.recBotCoe bot coe (some a) = coe a

Instances For

source
@[simp]
theorem WithBot.recBotCoe_bot {α : Type u_1} {C : WithBot α → Sort u_2} (d : C ⊥) (f : (a : α) → C ↑a) :
recBotCoe d f ⊥ = d
source
@[simp]
theorem WithBot.recBotCoe_coe {α : Type u_1} {C : WithBot α → Sort u_2} (d : C ⊥) (f : (a : α) → C ↑a) (x : α) :
recBotCoe d f ↑x = f x
source
def WithTop (α : Type u_2) :
Type u_2

Attach `⊤` to a type.

Equations

- WithTop α = Option α

Instances For

source
instance WithTop.instRepr {α : Type u_1} [Repr α] :
Repr (WithTop α)
Equations

- WithTop.instRepr = { reprPrec := fun (o : WithTop α) (x : ℕ) => match o with | none => Std.Format.text "⊤" | some a => Std.Format.text "↑" ++ repr a }

source
@[match_pattern]
def WithTop.some {α : Type u_1} :
α → WithTop α

The canonical map from `α` into `WithTop α`

Equations

- WithTop.some = some

Instances For

source
instance WithTop.coeTC {α : Type u_1} :
CoeTC α (WithTop α)
Equations

- WithTop.coeTC = { coe := WithTop.some }

source
instance WithTop.top {α : Type u_1} :
Top (WithTop α)
Equations

- WithTop.top = { top := none }

source
instance WithTop.inhabited {α : Type u_1} :
Inhabited (WithTop α)
Equations

- WithTop.inhabited = { default := ⊤ }

source
def WithTop.recTopCoe {α : Type u_1} {C : WithTop α → Sort u_2} (top : C ⊤) (coe : (a : α) → C ↑a) (n : WithTop α) :
C n

Recursor for `WithTop` using the preferred forms `⊤` and `↑a`.

Equations

- WithTop.recTopCoe top coe none = top
- WithTop.recTopCoe top coe (some a) = coe a

Instances For

source
@[simp]
theorem WithTop.recTopCoe_top {α : Type u_1} {C : WithTop α → Sort u_2} (d : C ⊤) (f : (a : α) → C ↑a) :
recTopCoe d f ⊤ = d
source
@[simp]
theorem WithTop.recTopCoe_coe {α : Type u_1} {C : WithTop α → Sort u_2} (d : C ⊤) (f : (a : α) → C ↑a) (x : α) :
recTopCoe d f ↑x = f x