@[specialize #[]]

def Lean.LocalContext.firstDeclM {m : Type u → Type v} [Monad m] [Alternative m] {β : Type u} (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m β) : m β

Return the result of f on the first local declaration on which f succeeds.

Equations

• lctx.firstDeclM f = do let __do_lift ← lctx.findDeclM? (optional ∘ f) match __do_lift with | none => failure | some b => pure b

@[specialize #[]]

def Lean.LocalContext.lastDeclM {m : Type u → Type v} [Monad m] [Alternative m] {β : Type u} (lctx : Lean.LocalContext) (f : Lean.LocalDecl → m β) : m β

Return the result of f on the last local declaration on which f succeeds.

Equations

• lctx.lastDeclM f = do let __do_lift ← lctx.findDeclRevM? (optional ∘ f) match __do_lift with | none => failure | some b => pure b