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 <$> Except.error e = Except.error e

@[simp]

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

def Except.pmap {ε : Type u} {α β : Type v} (x : Except ε α) (f : (a : α) → x = Except.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 : α) → Except.error e = Except.ok a → β) : (Except.error e).pmap f = Except.error e

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ExceptT.run_mk {ε α : Type u} {m : Type u → Type v} (x : m (Except ε α)) : (ExceptT.mk x).run = x

@[simp]

theorem ExceptT.mk_run {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} (x : ExceptT ε m α) : ExceptT.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 <$> ExceptT.mk x = ExceptT.mk ((fun (x : Except ε α) => f <$> x) <$> x)