Documentation

Mathlib.Lean.LocalContext

@[specialize #[]]
def Lean.LocalContext.firstDeclM {m : Type u → Type v} [inst : Monad m] [inst : 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
@[specialize #[]]
def Lean.LocalContext.lastDeclM {m : Type u → Type v} [inst : Monad m] [inst : 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