instance Sum.instDecidableEqSum : {α : Type u_1} → {β : Type u_2} → [inst : DecidableEq α] → [inst : DecidableEq β] → DecidableEq (α ⊕ β)

Equations

• Sum.instDecidableEqSum = Sum.decEqSum✝

instance Sum.instBEqSum : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst : BEq β] → BEq (α ⊕ β)

Equations

• Sum.instBEqSum = { beq := Sum.beqSum✝ }

def Sum.getLeft? {α : Type u_1} {β : Type u_2} : α ⊕ β → Option α

Check if a sum is inl and if so, retrieve its contents.

Equations

• Sum.getLeft? x = match x with | Sum.inl a => some a | Sum.inr val => none

def Sum.getRight? {α : Type u_1} {β : Type u_2} : α ⊕ β → Option β

Check if a sum is inr and if so, retrieve its contents.

Equations

• Sum.getRight? x = match x with | Sum.inr b => some b | Sum.inl val => none