mkInstanceNameForTypeExpr — Mathlib

Lean4
/-- Similar to `mkInstanceName`, but for a `Expr` type. -/
def mkInstanceNameForTypeExpr (type : Expr) : TermElabM Name := do
  let result ←
    do
      let ref ← IO.mkRef ""
      Meta.forEachExpr type fun e => do
          if e.isForall then
            ref.modify (· ++ "ForAll")
          else if e.isProp then
            ref.modify (· ++ "Prop")
          else if e.isType then
            ref.modify (· ++ "Type")
          else if e.isSort then
            ref.modify (· ++ "Sort")
          else if e.isConst then
            match e.constName!.eraseMacroScopes with
            | .str _ str =>
              if str.front.isLower then
                ref.modify (· ++ str.capitalize)
              else
                ref.modify (· ++ str)
            | _ =>
              pure ()
      ref.get
  liftMacroM <| mkUnusedBaseName <| Name.mkSimple ("inst" ++ result)
Похожие утверждения