Additional methods about LocalContext #
@[specialize #[]]
def
Lean.LocalContext.firstDeclM
{m : Type u → Type v}
[Monad m]
[Alternative m]
{β : Type u}
(lctx : LocalContext)
(f : 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 : LocalContext)
(f : LocalDecl → m β)
:
m β
Return the result of f on the last local declaration on which f succeeds.