mathlib documentation

core.init.meta.interaction_monad

meta inductive interaction_monad.result  :
Type → Type uType 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

@[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} :
result state αresult state α

meta def interaction_monad  :
Type → Type uType u

meta def interaction_monad_fmap {state : Type} {α : Type u} {β : Type v} :
(α → β)interaction_monad state αinteraction_monad state β

meta def interaction_monad_bind {state : Type} {α : Type u} {β : Type v} :
interaction_monad state α(α → interaction_monad state β)interaction_monad state β

meta def interaction_monad_return {state : Type} {α : Type u} :
α → interaction_monad state α

meta def interaction_monad_orelse {state : Type} {α : Type u} :
interaction_monad state αinteraction_monad state αinteraction_monad state α

meta def interaction_monad_seq {state : Type} {α : Type u} {β : Type v} :
interaction_monad state αinteraction_monad state βinteraction_monad state β

@[instance]
meta def interaction_monad.monad {state : Type} :

meta def interaction_monad.mk_exception {state : Type} {α : Type u} {β : Type v} [has_to_format β] :
β → option exprstate → result state α

meta def interaction_monad.fail {state : Type} {α : Type u} {β : Type v} [has_to_format β] :
β → interaction_monad state α

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} :
interaction_monad state αinteraction_monad state α(bool := tt)interaction_monad state α

@[instance]
meta def interaction_monad.monad_fail {state : Type} :

meta def interaction_monad.bracket {state : Type} {α β γ : Type u_1} :
interaction_monad state αinteraction_monad state βinteraction_monad state γinteraction_monad state β