findTargetName — Mathlib

Lean4
/-- Find the target name of `pre` and all created auxiliary declarations. -/
def findTargetName (env : Environment) (src pre tgt_pre : Name) : CoreM Name :=
  /- This covers auxiliary declarations like `match_i` and `proof_i`. -/

  if let some post := pre.isPrefixOf? src then return tgt_pre ++ post
  else
    if let some post := privateToUserName? src then
      match findTranslation? env post.getPrefix with
        -- this is an equation lemma for a declaration without `to_additive`. We will skip this.

      | none => return src
      | some addName => return src.updatePrefix <| mkPrivateName env addName
    else if src.hasMacroScopes then mkFreshUserName src.eraseMacroScopes else throwError"internal @[to_additive] error."
Похожие утверждения