def instDecidableEqExcept_batteries.decEq {ε✝ : Type u_1} {α✝ : Type u_2} [DecidableEq ε✝] [DecidableEq α✝] (x✝ x✝¹ : Except ε✝ α✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqExcept_batteries.decEq (Except.error a) (Except.error b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqExcept_batteries.decEq (Except.error a) (Except.ok a_1) = isFalse ⋯
• instDecidableEqExcept_batteries.decEq (Except.ok a) (Except.error a_1) = isFalse ⋯
• instDecidableEqExcept_batteries.decEq (Except.ok a) (Except.ok b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instDecidableEqExcept_batteries {ε✝ : Type u_1} {α✝ : Type u_2} [DecidableEq ε✝] [DecidableEq α✝] : DecidableEq (Except ε✝ α✝)

Equations

• instDecidableEqExcept_batteries = instDecidableEqExcept_batteries.decEq

def Except.emoji {ε : Type u_1} {α : Type u_2} : Except ε α → String

Visualize an Except using a checkmark or a cross.

Equations

• (Except.error a).emoji = Lean.crossEmoji
• (Except.ok a).emoji = Lean.checkEmoji

@[simp]

theorem Except.map_error {α β : Type u_1} {ε : Type u} (f : α → β) (e : ε) : f <$> error e = error e

@[simp]

theorem Except.map_ok {α β : Type u_1} {ε : Type u} (f : α → β) (x : α) : f <$> ok x = ok (f x)

def Except.pmap {ε : Type u} {α β : Type v} (x : Except ε α) (f : (a : α) → x = ok a → β) : Except ε β

Map a function over an Except value, using a proof that the value is .ok.

Equations

• (Except.error e).pmap f_2 = Except.error e
• (Except.ok a).pmap f_2 = Except.ok (f_2 a ⋯)

@[simp]

theorem Except.pmap_error {ε : Type u} {α β : Type v} (e : ε) (f : (a : α) → error e = ok a → β) : (error e).pmap f = error e

@[simp]

theorem Except.pmap_ok {ε : Type u} {α β : Type v} (a : α) (f : (a' : α) → ok a = ok a' → β) : (ok a).pmap f = ok (f a ⋯)

@[simp]

theorem Except.pmap_id {ε : Type u} {α : Type v} (x : Except ε α) : (x.pmap fun (a : α) (x : x = ok a) => a) = x

@[simp]

theorem Except.map_pmap {β γ : Type u_1} {ε : Type u_2} {α : Type u_1} (g : β → γ) (x : Except ε α) (f : (a : α) → x = ok a → β) : g <$> x.pmap f = x.pmap fun (a : α) (h : x = ok a) => g (f a h)

@[simp]

theorem ExceptT.mk_run {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} (x : ExceptT ε m α) : mk x.run = x

@[simp]

theorem ExceptT.map_mk {m : Type u_1 → Type u_2} {α β ε : Type u_1} [Monad m] [LawfulMonad m] (f : α → β) (x : m (Except ε α)) : f <$> mk x = mk ((fun (x : Except ε α) => f <$> x) <$> x)