def EStateM.Result.map {ε σ α β : Type u_1} (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_1} (f : α → β) (a : α) (s : σ) : map f (ok a s) = ok (f a) s

@[simp]

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

@[simp]

theorem EStateM.Result.map_eq_ok {ε σ α β : Type u_1} {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_1} (f : α → β) {x : Result ε σ α} {e : ε} {s : σ} : map f x = error e s ↔ x = error e s

@[simp]

theorem EStateM.dummySave_apply {σ : Type u_1} (s : σ) : dummySave s = PUnit.unit

@[simp]

theorem EStateM.dummyRestore_apply {σ : Type u_1} (s : σ) : dummyRestore s = Function.const PUnit s

@[simp]

theorem EStateM.run_pure {α σ ε : Type u_1} (x : α) (s : σ) : (pure x).run s = Result.ok x s

@[simp]

theorem EStateM.run'_pure {α σ ε : Type u_1} (x : α) (s : σ) : (pure x).run' s = some x

@[simp]

theorem EStateM.run_bind {ε σ α β : Type u_1} (x : EStateM ε σ α) (f : α → EStateM ε σ β) (s : σ) : (x >>= f).run s = match x.run s with | Result.ok a s => (f a).run s | Result.error e s => Result.error e s

@[simp]

theorem EStateM.run'_bind {ε σ α β : Type u_1} (x : EStateM ε σ α) (f : α → EStateM ε σ β) (s : σ) : (x >>= f).run' s = match x.run s with | Result.ok a s => (f a).run' s | Result.error a a_1 => none

@[simp]

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

@[simp]

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

theorem EStateM.run_seq {ε σ α β : Type u_1} (f : EStateM ε σ (α → β)) (x : EStateM ε σ α) (s : σ) : (f <*> x).run s = match f.run s with | Result.ok g s => Result.map g (x.run s) | Result.error e s => Result.error e s

theorem EStateM.run'_seq {ε σ α β : Type u_1} (f : EStateM ε σ (α → β)) (x : EStateM ε σ α) (s : σ) : (f <*> x).run' s = match f.run s with | Result.ok g s => Option.map g (x.run' s) | Result.error a a_1 => none

@[simp]

theorem EStateM.run_seqLeft {ε σ α β : Type u_1} (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ) : (x <* y).run s = match x.run s with | Result.ok v s => Result.map (fun (x : β) => v) (y.run s) | Result.error e s => Result.error e s

@[simp]

theorem EStateM.run'_seqLeft {ε σ α β : Type u_1} (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ) : (x <* y).run' s = match x.run s with | Result.ok v s => Option.map (fun (x : β) => v) (y.run' s) | Result.error a a_1 => none

@[simp]

theorem EStateM.run_seqRight {ε σ α β : Type u_1} (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ) : (x *> y).run s = match x.run s with | Result.ok a s => y.run s | Result.error e s => Result.error e s

@[simp]

theorem EStateM.run'_seqRight {ε σ α β : Type u_1} (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ) : (x *> y).run' s = match x.run s with | Result.ok a s => y.run' s | Result.error a a_1 => none

@[simp]

theorem EStateM.run_get {σ ε : Type u_1} (s : σ) : get.run s = Result.ok s s

@[simp]

theorem EStateM.run'_get {σ ε : Type u_1} (s : σ) : get.run' s = some s

@[simp]

theorem EStateM.run_set {σ ε : Type u_1} (v s : σ) : (set v).run s = Result.ok PUnit.unit v

@[simp]

theorem EStateM.run'_set {σ ε : Type u_1} (v s : σ) : (set v).run' s = some PUnit.unit

@[simp]

theorem EStateM.run_modify {σ ε : Type u_1} (f : σ → σ) (s : σ) : (modify f).run s = Result.ok PUnit.unit (f s)

@[simp]

theorem EStateM.run'_modify {σ ε : Type u_1} (f : σ → σ) (s : σ) : (modify f).run' s = some PUnit.unit

@[simp]

theorem EStateM.run_modifyGet {σ α ε : Type u_1} (f : σ → α × σ) (s : σ) : (modifyGet f).run s = Result.ok (f s).fst (f s).snd

@[simp]

theorem EStateM.run'_modifyGet {σ α ε : Type u_1} (f : σ → α × σ) (s : σ) : (modifyGet f).run' s = some (f s).fst

@[simp]

theorem EStateM.run_getModify {σ ε : Type u_1} {s : σ} (f : σ → σ) : (getModify f).run s = Result.ok s (f s)

@[simp]

theorem EStateM.run'_getModify {σ ε : Type u_1} (f : σ → σ) (s : σ) : (getModify f).run' s = some s

@[simp]

theorem EStateM.run_throw {ε σ α : Type u_1} (e : ε) (s : σ) : (throw e).run s = Result.error e s

@[simp]

theorem EStateM.run'_throw {ε σ α : Type u_1} (e : ε) (s : σ) : (throw e).run' s = none

@[simp]

theorem EStateM.run_orElse {σ ε α δ : Type u_1} [h : Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (s : σ) : (x₁ <|> x₂).run s = match x₁.run s with | Result.ok x s => Result.ok x s | Result.error a s' => x₂.run (Backtrackable.restore s' (Backtrackable.save s))

@[simp]

theorem EStateM.run'_orElse {σ ε α δ : Type u_1} [h : Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (s : σ) : (x₁ <|> x₂).run' s = match x₁.run s with | Result.ok x a => some x | Result.error a s' => x₂.run' (Backtrackable.restore s' (Backtrackable.save s))

@[simp]

theorem EStateM.run_tryCatch {σ ε α δ : Type u_1} [h : Backtrackable δ σ] (body : EStateM ε σ α) (handler : ε → EStateM ε σ α) (s : σ) : (tryCatch body handler).run s = match body.run s with | Result.ok x s => Result.ok x s | Result.error e s' => (handler e).run (Backtrackable.restore s' (Backtrackable.save s))

@[simp]

theorem EStateM.run'_tryCatch {σ ε α δ : Type u_1} [h : Backtrackable δ σ] (body : EStateM ε σ α) (handler : ε → EStateM ε σ α) (s : σ) : (tryCatch body handler).run' s = match body.run s with | Result.ok x a => some x | Result.error e s' => (handler e).run' (Backtrackable.restore s' (Backtrackable.save s))

@[simp]

theorem EStateM.run_adaptExcept {ε σ α : Type u_1} (f : ε → ε) (x : EStateM ε σ α) (s : σ) : (adaptExcept f x).run s = match x.run s with | Result.ok x s => Result.ok x s | Result.error e s => Result.error (f e) s

@[simp]

theorem EStateM.run'_adaptExcept {ε σ α : Type u_1} (f : ε → ε) (x : EStateM ε σ α) (s : σ) : (adaptExcept f x).run' s = x.run' s

@[simp]

theorem EStateM.run_tryFinally' {ε σ α β : Type u_1} (x : EStateM ε σ α) (h : Option α → EStateM ε σ β) (s : σ) : (tryFinally' x h).run s = match x.run s with | Result.ok a s => match (h (some a)).run s with | Result.ok b s => Result.ok (a, b) s | Result.error e s => Result.error e s | Result.error e₁ s => match (h none).run s with | Result.ok a s => Result.error e₁ s | Result.error e₂ s => Result.error e₂ s

@[simp]

theorem EStateM.run'_tryFinally' {ε σ α β : Type u_1} (x : EStateM ε σ α) (h : Option α → EStateM ε σ β) (s : σ) : (tryFinally' x h).run' s = match x.run s with | Result.ok a s => Option.map (fun (x : β) => (a, x)) ((h (some a)).run' s) | Result.error a a_1 => none

@[simp]

theorem EStateM.run_fromStateM {σ α ε : Type} (x : StateM σ α) (s : σ) : (fromStateM x).run s = Result.ok (StateT.run x s).fst (StateT.run x s).snd

@[simp]

theorem EStateM.run'_fromStateM {σ α ε : Type} (x : StateM σ α) (s : σ) : (fromStateM x).run' s = some (StateT.run' x s)

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

theorem EStateM.ext_iff {ε σ α : Type u_1} {x y : EStateM ε σ α} : x = y ↔ ∀ (s : σ), x.run s = y.run s