@[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.
Instances For
@[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.