mathlib documentation

meta def interaction_monad.result_to_string {state : Type} {α : Type u} [has_to_string α] (a : result state α) :

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 : ℕ) (a : result state α) :

meta def interaction_monad (state : Type) (α : 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 β) :

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) :

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) :

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 γ) :