mathlib documentation

core / init.control.monad_fail

@[class]

structure monad_fail (m : Type u → Type v) :

Type (max (u+1) v)

fail : Π {a : Type ?}, string → m a

Instances

def match_failed {α : Type u} {m : Type u → Type v} [monad_fail m] :

m α

Equations

match_failed = monad_fail.fail "match failed"

@[protected, instance]

def monad_fail_lift (m n : Type u → Type v) [monad n] [monad_fail m] [has_monad_lift m n] :

Equations

monad_fail_lift m n = {fail := λ (α : Type u) (s : string), monad_lift (monad_fail.fail s)}