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 : ℕ) => 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 : ℕ) => 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

def ENat : Type

Extended natural numbers ℕ∞ = WithTop ℕ.

Equations

• ℕ∞ = WithTop ℕ

def «termℕ∞» : Lean.ParserDescr

Extended natural numbers ℕ∞ = WithTop ℕ.

Equations

• «termℕ∞» = Lean.ParserDescr.node `termℕ∞ 1024 (Lean.ParserDescr.symbol "ℕ∞")

instance ENat.instNatCast : NatCast ℕ∞

Equations

• ENat.instNatCast = { natCast := WithTop.some }

def ENat.recTopCoe {C : ℕ∞ → Sort u_2} (top : C ⊤) (coe : (a : ℕ) → C ↑a) (n : ℕ∞) : C n

Recursor for ENat using the preferred forms ⊤ and ↑a.

Equations

• ENat.recTopCoe top coe none = top
• ENat.recTopCoe top coe (some a) = coe a

@[simp]

theorem ENat.recTopCoe_top {C : ℕ∞ → Sort u_2} (d : C ⊤) (f : (a : ℕ) → C ↑a) : ENat.recTopCoe d f ⊤ = d

@[simp]

theorem ENat.recTopCoe_coe {C : ℕ∞ → Sort u_2} (d : C ⊤) (f : (a : ℕ) → C ↑a) (x : ℕ) : ENat.recTopCoe d f ↑x = f x

def PNat : Type

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Equations

• ℕ+ = { n : ℕ // 0 < n }

def «termℕ+» : Lean.ParserDescr

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Equations

• «termℕ+» = Lean.ParserDescr.node `termℕ+ 1024 (Lean.ParserDescr.symbol "ℕ+")

def PNat.val : ℕ+ → ℕ

The underlying natural number

Equations

• PNat.val = Subtype.val

instance coePNatNat : Coe ℕ+ ℕ

Equations

• coePNatNat = { coe := PNat.val }

instance instReprPNat : Repr ℕ+

Equations

• instReprPNat = { reprPrec := fun (n : ℕ+) (n' : ℕ) => reprPrec n.val n' }