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

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

Equations

• EStateM.Result.map f (EStateM.Result.ok a s') = EStateM.Result.ok (f a) s'
• EStateM.Result.map f (EStateM.Result.error e s') = EStateM.Result.error e s'

@[simp]

theorem EStateM.Result.map_ok {ε σ α β : Type u} (f : α → β) (a : α) (s : σ) : map f (ok a s) = ok (f a) s

@[simp]

theorem EStateM.Result.map_error {ε σ α β : Type u} (f : α → β) (e : ε) (s : σ) : map f (error e s) = error e s

@[simp]

theorem EStateM.Result.map_eq_ok {ε σ α β : Type u} (f : α → β) (x : Result ε σ α) (b : β) (s : σ) : map f x = ok b s ↔ ∃ (a : α), x = ok a s ∧ b = f a

@[simp]

theorem EStateM.Result.map_eq_error {ε σ α β : Type u} (f : α → β) (x : Result ε σ α) (e : ε) (s : σ) : map f x = error e s ↔ x = error e s

@[simp]

theorem EStateM.run_map {α β ε σ : Type u_1} {s : σ} (f : α → β) (x : EStateM ε σ α) : (f <$> x).run s = Result.map f (x.run s)

theorem EStateM.ext {ε σ α : Type u} (x y : EStateM ε σ α) (h : ∀ (s : σ), x.run s = y.run s) : x = y