mathlib documentation

core / init.control.monad_fail

@[class]
structure monad_fail (m : Type u Type v) :
Type (max (u+1) v)
Instances of this typeclass
Instances of other typeclasses for monad_fail
  • monad_fail.has_sizeof_inst
def match_failed {α : Type u} {m : Type u Type v} [monad_fail m] :
m α
Equations
@[protected, instance]
def monad_fail_lift (m n : Type u Type v) [monad n] [monad_fail m] [has_monad_lift m n] :
Equations