Order-related type synonyms

In this file we define WithBot and WithTop.

def WithBot (α : Type u_2) : Type u_2

Attach ⊥ to a type.

Equations

• WithBot α = Option α

def WithTop (α : Type u_2) : Type u_2

Attach ⊤ to a type.

Equations

• WithTop α = Option α

@[implicit_reducible]

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 }

@[implicit_reducible]

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 WithBot.some {α : Type u_1} : α → WithBot α

The canonical map from α into WithBot α

Equations

• WithBot.some = some

@[match_pattern]

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

The canonical map from α into WithTop α

Equations

• WithTop.some = some

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• WithBot.bot = { bot := none }

@[implicit_reducible]

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

Equations

• WithTop.top = { top := none }

@[implicit_reducible]

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

Equations

• WithBot.inhabited = { default := ⊥ }

@[implicit_reducible]

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

Equations

• WithTop.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

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 bot coe none = bot
• WithTop.recTopCoe 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) : recBotCoe d f ⊥ = d

@[simp]

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

@[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

@[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