mathlib3 documentation

core / init.meta.interaction_monad

source
meta inductive interaction_monad.result (state : Type) (α : Type u) :
Type u
Instances for interaction_monad.result
source
meta def interaction_monad.result_to_string {state : Type} {α : Type u} [has_to_string α] :
interaction_monad.result state α → string
source
@[protected, instance]
meta def interaction_monad.result_has_string {state : Type} {α : Type u} [has_to_string α] :
has_to_string (interaction_monad.result state α)
source
meta def interaction_monad.result.clamp_pos {state : Type} {α : Type u} (line0 line col : ℕ) :
interaction_monad.result state α → interaction_monad.result state α
source
@[reducible]
meta def interaction_monad (state : Type) (α : Type u) :
Type u
source
meta def interaction_monad_fmap {state : Type} {α : Type u} {β : Type v} (f : α → β) (t : interaction_monad state α) :
interaction_monad state β
source
meta def interaction_monad_bind {state : Type} {α : Type u} {β : Type v} (t₁ : interaction_monad state α) (t₂ : α → interaction_monad state β) :
interaction_monad state β
source
meta def interaction_monad_return {state : Type} {α : Type u} (a : α) :
interaction_monad state α
source
meta def interaction_monad_orelse {state : Type} {α : Type u} (t₁ t₂ : interaction_monad state α) :
interaction_monad state α
source
meta def interaction_monad_seq {state : Type} {α : Type u} {β : Type v} (t₁ : interaction_monad state α) (t₂ : interaction_monad state β) :
interaction_monad state β
source
@[protected, instance]
meta def interaction_monad.monad {state : Type} :
monad (interaction_monad state)
source
meta def interaction_monad.mk_exception {state : Type} {α : Type u} {β : Type v} [has_to_format β] (msg : β) (ref : option expr) (s : state) :
interaction_monad.result state α
source
meta def interaction_monad.fail {state : Type} {α : Type u} {β : Type v} [has_to_format β] (msg : β) :
interaction_monad state α
source
meta def interaction_monad.silent_fail {state : Type} {α : Type u} :
interaction_monad state α
source
meta def interaction_monad.failed {state : Type} {α : Type u} :
interaction_monad state α
source
meta def interaction_monad.orelse' {state : Type} {α : Type u} (t₁ t₂ : interaction_monad state α) (use_first_ex : bool := bool.tt) :
interaction_monad state α

Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard orelse uses the second.

source
@[protected, instance]
meta def interaction_monad.monad_fail {state : Type} :
monad_fail (interaction_monad state)
source
meta def interaction_monad.bracket {state : Type} {α β γ : Type u_1} (x : interaction_monad state α) (inside : interaction_monad state β) (y : interaction_monad state γ) :
interaction_monad state β