@[specialize #[]]
def
Lean.LocalContext.firstDeclM
{m : Type u → Type v}
[inst : Monad m]
[inst : 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
- Lean.LocalContext.firstDeclM lctx f = do let __do_lift ← Lean.LocalContext.findDeclM? lctx (optional ∘ f) match __do_lift with | none => failure | some b => pure b
@[specialize #[]]
def
Lean.LocalContext.lastDeclM
{m : Type u → Type v}
[inst : Monad m]
[inst : 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
- Lean.LocalContext.lastDeclM lctx f = do let __do_lift ← Lean.LocalContext.findDeclRevM? lctx (optional ∘ f) match __do_lift with | none => failure | some b => pure b