Documentation

Mathlib.Lean.LocalContext

Additional methods about LocalContext #

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

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

Equations
  • lctx.firstDeclM f = do let __do_liftlctx.findDeclM? (optional f) match __do_lift with | none => failure | some b => pure b
Instances For
    @[specialize #[]]
    def Lean.LocalContext.lastDeclM {m : Type u → Type v} [Monad m] [Alternative m] {β : Type u} (lctx : Lean.LocalContext) (f : Lean.LocalDeclm β) :
    m β

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

    Equations
    • lctx.lastDeclM f = do let __do_liftlctx.findDeclRevM? (optional f) match __do_lift with | none => failure | some b => pure b
    Instances For