Documentation

Batteries.Lean.EStateM

source
def EStateM.Result.map {ε σ α β : Type u} (f : α → β) (x : EStateM.Result ε σ α) :
EStateM.Result ε σ β

Map a function over an EStateM.Result, preserving states and errors.

Equations
Instances For
    source
    @[simp]
    theorem EStateM.Result.map_ok {ε σ α β : Type u} (f : α → β) (a : α) (s : σ) :
    EStateM.Result.map f (EStateM.Result.ok a s) = EStateM.Result.ok (f a) s
    source
    @[simp]
    theorem EStateM.Result.map_error {ε σ α β : Type u} (f : α → β) (e : ε) (s : σ) :
    EStateM.Result.map f (EStateM.Result.error e s) = EStateM.Result.error e s
    source
    @[simp]
    theorem EStateM.Result.map_eq_ok {ε σ α β : Type u} (f : α → β) (x : EStateM.Result ε σ α) (b : β) (s : σ) :
    EStateM.Result.map f x = EStateM.Result.ok b s ↔ ∃ (a : α), x = EStateM.Result.ok a s ∧ b = f a
    source
    @[simp]
    theorem EStateM.Result.map_eq_error {ε σ α β : Type u} (f : α → β) (x : EStateM.Result ε σ α) (e : ε) (s : σ) :
    EStateM.Result.map f x = EStateM.Result.error e s ↔ x = EStateM.Result.error e s
    source
    @[simp]
    theorem EStateM.run_map {α β ε σ : Type u_1} {s : σ} (f : α → β) (x : EStateM ε σ α) :
    (f <$> x).run s = EStateM.Result.map f (x.run s)
    source
    theorem EStateM.ext {ε σ α : Type u} (x y : EStateM ε σ α) (h : ∀ (s : σ), x.run s = y.run s) :
    x = y