inductive Data.Either (α : Type u) (β : Type v) : Type (max u v)

Either α β is a sum type: either Left α or Right β.

Right-biased: Functor, Monad act on the Right case. $$\text{Either}(\alpha, \beta) \cong \alpha + \beta$$

• left {α : Type u} {β : Type v} : α → Either α β

  The left case, typically representing an error or alternative.

• right {α : Type u} {β : Type v} : β → Either α β

  The right case, typically representing success.

@[implicit_reducible]

instance Data.instBEqEither {α✝ : Type u_1} {β✝ : Type u_2} [BEq α✝] [BEq β✝] : BEq (Either α✝ β✝)

Equations

• Data.instBEqEither = { beq := Data.instBEqEither.beq }

def Data.instBEqEither.beq {α✝ : Type u_1} {β✝ : Type u_2} [BEq α✝] [BEq β✝] : Either α✝ β✝ → Either α✝ β✝ → Bool

Equations

• Data.instBEqEither.beq (Data.Either.left a) (Data.Either.left b) = (a == b)
• Data.instBEqEither.beq (Data.Either.right a) (Data.Either.right b) = (a == b)
• Data.instBEqEither.beq x✝¹ x✝ = false

def Data.instOrdEither.ord {α✝ : Type u_1} {β✝ : Type u_2} [Ord α✝] [Ord β✝] : Either α✝ β✝ → Either α✝ β✝ → Ordering

Equations

• Data.instOrdEither.ord (Data.Either.left a) (Data.Either.left b) = (compare a b).then Ordering.eq
• Data.instOrdEither.ord (Data.Either.left a) x✝ = Ordering.lt
• Data.instOrdEither.ord x✝ (Data.Either.left a) = Ordering.gt
• Data.instOrdEither.ord (Data.Either.right a) (Data.Either.right b) = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Data.instOrdEither {α✝ : Type u_1} {β✝ : Type u_2} [Ord α✝] [Ord β✝] : Ord (Either α✝ β✝)

Equations

• Data.instOrdEither = { compare := Data.instOrdEither.ord }

@[implicit_reducible]

instance Data.instReprEither {α✝ : Type u_1} {β✝ : Type u_2} [Repr α✝] [Repr β✝] : Repr (Either α✝ β✝)

Equations

• Data.instReprEither = { reprPrec := Data.instReprEither.repr }

def Data.instReprEither.repr {α✝ : Type u_1} {β✝ : Type u_2} [Repr α✝] [Repr β✝] : Either α✝ β✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Data.instHashableEither.hash {α✝ : Type u_1} {β✝ : Type u_2} [Hashable α✝] [Hashable β✝] : Either α✝ β✝ → UInt64

Equations

• Data.instHashableEither.hash (Data.Either.left a) = mixHash 0 (hash a)
• Data.instHashableEither.hash (Data.Either.right a) = mixHash 1 (hash a)

@[implicit_reducible]

instance Data.instHashableEither {α✝ : Type u_1} {β✝ : Type u_2} [Hashable α✝] [Hashable β✝] : Hashable (Either α✝ β✝)

Equations

• Data.instHashableEither = { hash := Data.instHashableEither.hash }

@[inline]

def Data.Either.isLeft {α : Type u_1} {β : Type u_2} : Either α β → Bool

Test if a value is Left. $$\text{isLeft}(x) = \begin{cases} \text{true} & \text{if } x = \text{Left}(a) \\ \text{false} & \text{if } x = \text{Right}(b) \end{cases}$$

Equations

• (Data.Either.left a).isLeft = true
• (Data.Either.right a).isLeft = false

@[inline]

def Data.Either.isRight {α : Type u_1} {β : Type u_2} : Either α β → Bool

Test if a value is Right. $$\text{isRight}(x) = \neg\,\text{isLeft}(x)$$

Equations

• (Data.Either.left a).isRight = false
• (Data.Either.right a).isRight = true

@[inline]

def Data.Either.fromLeft {α : Type u_1} {β : Type u_2} (default : α) : Either α β → α

Extract from Left, or return a default. $$\text{fromLeft}(d, \text{Left}(a)) = a, \quad \text{fromLeft}(d, \text{Right}(b)) = d$$

Equations

• Data.Either.fromLeft default (Data.Either.left a) = a
• Data.Either.fromLeft default (Data.Either.right a) = default

@[inline]

def Data.Either.fromRight {β : Type u_1} {α : Type u_2} (default : β) : Either α β → β

Extract from Right, or return a default. $$\text{fromRight}(d, \text{Right}(b)) = b, \quad \text{fromRight}(d, \text{Left}(a)) = d$$

Equations

• Data.Either.fromRight default (Data.Either.left a) = default
• Data.Either.fromRight default (Data.Either.right b) = b

@[inline]

def Data.Either.either {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : α → γ) (g : β → γ) : Either α β → γ

Case analysis: apply f to Left, g to Right. $$\text{either}(f, g, \text{Left}(a)) = f(a), \quad \text{either}(f, g, \text{Right}(b)) = g(b)$$

Equations

• Data.Either.either f g (Data.Either.left a) = f a
• Data.Either.either f g (Data.Either.right a) = g a

@[inline]

def Data.Either.mapLeft {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : α → γ) : Either α β → Either γ β

Map over the left component. $$\text{mapLeft}(f, \text{Left}(a)) = \text{Left}(f(a))$$

Equations

• Data.Either.mapLeft f (Data.Either.left a) = Data.Either.left (f a)
• Data.Either.mapLeft f (Data.Either.right a) = Data.Either.right a

@[inline]

def Data.Either.mapRight {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) : Either α β → Either α γ

Map over the right component. $$\text{mapRight}(f, \text{Right}(b)) = \text{Right}(f(b))$$

Equations

• Data.Either.mapRight f (Data.Either.left a) = Data.Either.left a
• Data.Either.mapRight f (Data.Either.right b) = Data.Either.right (f b)

@[inline]

def Data.Either.swap {α : Type u_1} {β : Type u_2} : Either α β → Either β α

Swap Left and Right. $$\text{swap}(\text{Left}(a)) = \text{Right}(a), \quad \text{swap}(\text{Right}(b)) = \text{Left}(b)$$

Equations

• (Data.Either.left a).swap = Data.Either.right a
• (Data.Either.right a).swap = Data.Either.left a

def Data.Either.partitionEithers {α : Type u_1} {β : Type u_2} (l : List (Either α β)) : List α × List β

Partition a list of Either into lefts and rights.

Given $[e_1, \ldots, e_n]$, produces $(ls, rs)$ where $ls$ are the Left values and $rs$ are the Right values.

Length preservation: $|ls| + |rs| = n$

Equations

• One or more equations did not get rendered due to their size.

theorem Data.Either.swap_swap {α : Type u_1} {β : Type u_2} (e : Either α β) : e.swap.swap = e

Swapping twice is identity.

theorem Data.Either.isLeft_not_isRight {α : Type u_1} {β : Type u_2} (e : Either α β) : e.isLeft = !e.isRight

isLeft and isRight are complementary.

theorem Data.Either.partitionEithers_length {α : Type u_1} {β : Type u_2} (l : List (Either α β)) : match partitionEithers l with | (ls, rs) => ls.length + rs.length = l.length

Partition preserves total count: $$|\text{fst}(\text{partitionEithers}(l))| + |\text{snd}(\text{partitionEithers}(l))| = |l|$$

theorem Data.Either.map_id {α : Type u_1} {β : Type u_2} (e : Either α β) : mapRight id e = e

Identity law: map id = id for Either.

theorem Data.Either.map_comp {γ : Type u_1} {δ : Type u_2} {β : Type u_3} {α : Type u_4} (f : γ → δ) (g : β → γ) (e : Either α β) : mapRight (f ∘ g) e = mapRight f (mapRight g e)

Composition law: map (f ∘ g) = map f ∘ map g for Either.

@[implicit_reducible]

instance Data.Either.instFunctor {α : Type u_1} : Functor (Either α)

Equations

• Data.Either.instFunctor = { map := fun {α_1 β : Type ?u.15} => Data.Either.mapRight }

@[implicit_reducible]

instance Data.Either.instPure {α : Type u_1} : Pure (Either α)

Equations

• Data.Either.instPure = { pure := fun {α_1 : Type ?u.10} => Data.Either.right }

@[implicit_reducible]

instance Data.Either.instBind {α : Type u_1} : Bind (Either α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Either.instSeq {α : Type u_1} : Seq (Either α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Either.instApplicative {α : Type u_1} : Applicative (Either α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Either.instMonad {α : Type u_1} : Monad (Either α)

Equations

• Data.Either.instMonad = { toApplicative := Data.Either.instApplicative, toBind := Data.Either.instBind }

theorem Data.Either.pure_bind {β : Type u_1} {α : Type u_2} {γ : Type u_1} (a : β) (f : β → Either α γ) : right a >>= f = f a

Left identity: pure a >>= f = f a.

theorem Data.Either.bind_pure {α : Type u_1} {β : Type u_2} (e : Either α β) : e >>= right = e

Right identity: m >>= pure = m.

theorem Data.Either.bind_assoc {α : Type u_1} {β γ δ : Type u_2} (e : Either α β) (f : β → Either α γ) (g : γ → Either α δ) : e >>= f >>= g = e >>= fun (x : β) => f x >>= g

Associativity: (m >>= f) >>= g = m >>= (λ x → f x >>= g).

@[implicit_reducible]

instance Data.Either.instBifunctor : Bifunctor Either

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Either.instToString {α : Type u_1} {β : Type u_2} [ToString α] [ToString β] : ToString (Either α β)

Equations

• One or more equations did not get rendered due to their size.