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

Equations

• Sum.instDecidableEq = Sum.decEqSum✝

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

Equations

• Sum.instBEq = { 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.inl a).getLeft? = some a
• (Sum.inr val).getLeft? = 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.inr b).getRight? = some b
• (Sum.inl val).getRight? = none