mathlib documentation

core / init.meta.interaction_monad

meta inductive interaction_monad.result (state : Type) (α : Type u) :
Type u
  • success : Π (state : Type) (α : Type u), α → state → result state α
  • exception : Π (state : Type) (α : Type u), option (unitformat)option posstate → result state α
meta def interaction_monad.result_to_string {state : Type} {α : Type u} [has_to_string α] :
result state αstring
@[protected, instance]
meta def interaction_monad.result_has_string {state : Type} {α : Type u} [has_to_string α] :
meta def interaction_monad.result.clamp_pos {state : Type} {α : Type u} (line0 line col : ) :
result state αresult state α
meta def interaction_monad (state : Type) (α : Type u) :
Type u
meta def interaction_monad_fmap {state : Type} {α : Type u} {β : Type v} (f : α → β) (t : interaction_monad state α) :
meta def interaction_monad_bind {state : Type} {α : Type u} {β : Type v} (t₁ : interaction_monad state α) (t₂ : α → interaction_monad state β) :
meta def interaction_monad_return {state : Type} {α : Type u} (a : α) :
meta def interaction_monad_orelse {state : Type} {α : Type u} (t₁ t₂ : interaction_monad state α) :
meta def interaction_monad_seq {state : Type} {α : Type u} {β : Type v} (t₁ : interaction_monad state α) (t₂ : interaction_monad state β) :
@[protected, instance]
meta def interaction_monad.monad {state : Type} :
meta def interaction_monad.mk_exception {state : Type} {α : Type u} {β : Type v} [has_to_format β] (msg : β) (ref : option expr) (s : state) :
result state α
meta def interaction_monad.fail {state : Type} {α : Type u} {β : Type v} [has_to_format β] (msg : β) :
meta def interaction_monad.silent_fail {state : Type} {α : Type u} :
meta def interaction_monad.failed {state : Type} {α : Type u} :
meta def interaction_monad.orelse' {state : Type} {α : Type u} (t₁ t₂ : interaction_monad state α) (use_first_ex : bool := tt) :
@[protected, instance]
meta def interaction_monad.monad_fail {state : Type} :
meta def interaction_monad.bracket {state : Type} {α β γ : Type u_1} (x : interaction_monad state α) (inside : interaction_monad state β) (y : interaction_monad state γ) :