A dirt simple Instance handler

MyName.lean

import Lean.Elab.Deriving.Basic
import Lean.Elab.Deriving.Util

class MyName (α : Type) where
  nameID : α → String

namespace Lean.Elab.Deriving.MyName

open Lean.Parser.Term
open Meta

universe u

open Command

private def mkMyNameFuns (ctx : Context) (name : Name) : TermElabM Syntax := do
  let auxFunName := ctx.auxFunNames[0]!
  let header ← mkHeader ``MyName 1 ctx.typeInfos[0]!
  `(private def $(mkIdent auxFunName):ident $header.binders:bracketedBinder* : String := $(Syntax.mkStrLit name.toString))

def mkMyNameInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
  let ctx ← mkContext "myname" declName
  let cmds := #[← mkMyNameFuns ctx declName] ++ (← mkInstanceCmds ctx `MyName #[declName])
  return cmds

def mkMyNameHandler (declNames : Array Name) : CommandElabM Bool := do
  let cmds ← liftTermElabM none <| mkMyNameInstanceCmds declNames[0]!
  cmds.forM elabCommand
  return true

initialize
  registerBuiltinDerivingHandler `MyName mkMyNameHandler

end Lean.Elab.Deriving.MyName