getAuxDefOfDeclName — Mathlib

Lean4
/-- Get the auxiliary local declaration corresponding to the current declaration. If there are
multiple declarations it will throw. -/
def getAuxDefOfDeclName : TermElabM FVarId := do
  let some declName ← getDeclName? |
    throwError"no 'declName?'"
  let auxDeclMap := (← getLCtx).auxDeclToFullName
  let fvars :=
    auxDeclMap.foldl (init := []) fun fvars fvar fullName => if fullName = declName then fvars.concat fvar else fvars
  match fvars with
  | [] =>
    throwError"no auxiliary local declaration corresponding to the current declaration"
  | [fvar] =>
    return fvar
  | _ =>
    throwError"multiple local declarations corresponding to the current declaration"
Похожие утверждения