mathlib documentation

core / init.control.monad_fail

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

Equations
@[instance]
def monad_fail_lift (m n : Type uType v) [monad n] [monad_fail m] [has_monad_lift m n] :

Equations