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.

def WithBot (α : Type u_2) : Type u_2

Attach ⊥ to a type.

Equations

• WithBot α = Option α

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

Equations

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

@[match_pattern]

def WithBot.some {α : Type u_1} : α → WithBot α

The canonical map from α into WithBot α

Equations

• WithBot.some = some

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

Equations

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

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

Equations

• WithBot.bot = { bot := none }

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

Equations

• WithBot.inhabited = { default := ⊥ }

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

@[simp]

theorem WithBot.recBotCoe_bot {α : Type u_1} {C : WithBot α → Sort u_2} (d : C ⊥) (f : (a : α) → C ↑a) : WithBot.recBotCoe d f ⊥ = d

@[simp]

theorem WithBot.recBotCoe_coe {α : Type u_1} {C : WithBot α → Sort u_2} (d : C ⊥) (f : (a : α) → C ↑a) (x : α) : WithBot.recBotCoe d f ↑x = f x

def WithTop (α : Type u_2) : Type u_2

Attach ⊤ to a type.

Equations

• WithTop α = Option α

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

Equations

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

@[match_pattern]

def WithTop.some {α : Type u_1} : α → WithTop α

The canonical map from α into WithTop α

Equations

• WithTop.some = some

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

Equations

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

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

Equations

• WithTop.top = { top := none }

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

Equations

• WithTop.inhabited = { default := ⊤ }

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

@[simp]

theorem WithTop.recTopCoe_top {α : Type u_1} {C : WithTop α → Sort u_2} (d : C ⊤) (f : (a : α) → C ↑a) : WithTop.recTopCoe d f ⊤ = d

@[simp]

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