Documentation

Init.Data.Sum

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
Instances For
    def Sum.getRight? {α : Type u_1} {β : Type u_2} :
    α βOption β

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

    Equations
    Instances For