- success : Π (state : Type) (α : Type u), α → state → interaction_monad.result state α
- exception : Π (state : Type) (α : Type u), option (unit → format) → option pos → state → interaction_monad.result state α
def
interaction_monad.result_to_string
{state : Type}
{α : Type u}
[has_to_string α] :
interaction_monad.result state α → string
@[instance]
def
interaction_monad.result_has_string
{state : Type}
{α : Type u}
[has_to_string α] :
has_to_string (interaction_monad.result state α)
def
interaction_monad.result.clamp_pos
{state : Type}
{α : Type u} :
ℕ → ℕ → ℕ → interaction_monad.result state α → interaction_monad.result state α
def
interaction_monad_fmap
{state : Type}
{α : Type u}
{β : Type v} :
(α → β) → interaction_monad state α → interaction_monad state β
def
interaction_monad_bind
{state : Type}
{α : Type u}
{β : Type v} :
interaction_monad state α → (α → interaction_monad state β) → interaction_monad state β
def
interaction_monad_orelse
{state : Type}
{α : Type u} :
interaction_monad state α → interaction_monad state α → interaction_monad state α
def
interaction_monad_seq
{state : Type}
{α : Type u}
{β : Type v} :
interaction_monad state α → interaction_monad state β → interaction_monad state β
def
interaction_monad.mk_exception
{state : Type}
{α : Type u}
{β : Type v}
[has_to_format β] :
β → option expr → state → interaction_monad.result state α
def
interaction_monad.fail
{state : Type}
{α : Type u}
{β : Type v}
[has_to_format β] :
β → interaction_monad state α
def
interaction_monad.orelse'
{state : Type}
{α : Type u} :
interaction_monad state α → interaction_monad state α → (bool := bool.tt) → interaction_monad state α
@[instance]
def
interaction_monad.bracket
{state : Type}
{α β γ : Type u_1} :
interaction_monad state α → interaction_monad state β → interaction_monad state γ → interaction_monad state β