previousInstName — Mathlib

Lean4
/-- `previousInstName nm` takes as input a name `nm`, assuming that it is the name of an
auto-generated "nameless" `instance`.
If `nm` ends in `..._n`, where `n` is a number, it returns the same name, but with `_n` replaced
by `_(n-1)`, unless `n ≤ 1`, in which case it simply removes the `_n` suffix.
-/
def previousInstName : Name → Name
  | nm@(.str init tail) =>
    let last := tail.takeRightWhile (· != '_')
    let newTail :=
      match last.toNat? with
      | some (n + 2) => s! "_{n + 1}"
      | _ => ""
    let newTailPrefix := tail.dropRightWhile (· != '_')
    if newTailPrefix.isEmpty then nm
    else
      let newTail := (if newTailPrefix.back == '_' then newTailPrefix.dropRight 1 else newTailPrefix) ++ newTail
      .str init newTail
  | nm => nm
Похожие утверждения