Disjoint union of types #
This file defines basic operations on the the sum type α ⊕ β
.
α ⊕ β
is the type made of a copy of α
and a copy of β
. It is also called disjoint union.
Main declarations #
Sum.isLeft
: Returns whetherx : α ⊕ β
comes from the left component or not.Sum.isRight
: Returns whetherx : α ⊕ β
comes from the right component or not.Sum.getLeft
: Retrieves the left content of ax : α ⊕ β
that is known to come from the left.Sum.getRight
: Retrieves the right content ofx : α ⊕ β
that is known to come from the right.Sum.getLeft?
: Retrieves the left content ofx : α ⊕ β
as an option type or returnsnone
if it's coming from the right.Sum.getRight?
: Retrieves the right content ofx : α ⊕ β
as an option type or returnsnone
if it's coming from the left.Sum.map
: Mapsα ⊕ β
toγ ⊕ δ
component-wise.Sum.elim
: Nondependent eliminator/induction principle forα ⊕ β
.Sum.swap
: Mapsα ⊕ β
toβ ⊕ α
by swapping components.Sum.LiftRel
: The disjoint union of two relations.Sum.Lex
: Lexicographic order onα ⊕ β
induced by a relation onα
and a relation onβ
.
Further material #
See Std.Data.Sum.Lemmas
for theorems about these definitions.
Notes #
The definition of Sum
takes values in Type _
. This effectively forbids Prop
- valued sum types.
To this effect, we have PSum
, which takes value in Sort _
and carries a more complicated
universe signature in consequence. The Prop
version is Or
.
Equations
- Sum.instDecidableEqSum = Sum.decEqSum✝
Retrieve the contents from a sum known to be inl
.
Equations
- Sum.getLeft x✝ x = match x✝, x with | Sum.inl a, x => a
Instances For
Retrieve the contents from a sum known to be inr
.
Equations
- Sum.getRight x✝ x = match x✝, x with | Sum.inr b, x => b
Instances For
Lifts pointwise two relations between α
and γ
and between β
and δ
to a relation between
α ⊕ β
and γ ⊕ δ
.
- inl: ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : α → γ → Prop} {s : β → δ → Prop} {a : α} {c : γ}, r a c → Sum.LiftRel r s (Sum.inl a) (Sum.inl c)
- inr: ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : α → γ → Prop} {s : β → δ → Prop} {b : β} {d : δ}, s b d → Sum.LiftRel r s (Sum.inr b) (Sum.inr d)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Lexicographic order for sum. Sort all the inl a
before the inr b
, otherwise use the
respective order on α
or β
.
- inl: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α}, r a₁ a₂ → Sum.Lex r s (Sum.inl a₁) (Sum.inl a₂)
- inr: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {b₁ b₂ : β}, s b₁ b₂ → Sum.Lex r s (Sum.inr b₁) (Sum.inr b₂)
- sep: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (a : α) (b : β), Sum.Lex r s (Sum.inl a) (Sum.inr b)
Instances For
Equations
- One or more equations did not get rendered due to their size.