Documentation

Batteries.Lean.Except

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

Visualize an Except using a checkmark or a cross.

Equations
Instances For
    source
    @[simp]
    theorem Except.map_error {α β : Type u_1} {ε : Type u} (f : α → β) (e : ε) :
    f <$> error e = error e
    source
    @[simp]
    theorem Except.map_ok {α β : Type u_1} {ε : Type u} (f : α → β) (x : α) :
    f <$> ok x = ok (f x)
    source
    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
    Instances For
      source
      @[simp]
      theorem Except.pmap_error {ε : Type u} {α β : Type v} (e : ε) (f : (a : α) → error e = ok a → β) :
      (error e).pmap f = error e
      source
      @[simp]
      theorem Except.pmap_ok {ε : Type u} {α β : Type v} (a : α) (f : (a' : α) → ok a = ok a' → β) :
      (ok a).pmap f = ok (f a ⋯)
      source
      @[simp]
      theorem Except.pmap_id {ε : Type u} {α : Type v} (x : Except ε α) :
      (x.pmap fun (a : α) (x : x = ok a) => a) = x
      source
      @[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)
      source
      @[simp]
      theorem ExceptT.run_mk {ε α : Type u} {m : Type u → Type v} (x : m (Except ε α)) :
      (mk x).run = x
      source
      @[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
      source
      @[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)