Lean4
/-- Compile the definition `dv` by adding a second definition `dv✝` with the same body,
and registering a `csimp`-lemma `dv = dv✝`.
-/
def compileDefn (dv : DefinitionVal) : MetaM Unit := do
if ((← getEnv).getModuleIdxFor? dv.name).isNone then
-- If it's in the same module then we can safely just call `compileDecl`
-- on the original definition
return ← compileDecl <| .defnDecl dv
let name ← mkFreshUserName dv.name
addAndCompile' <| .defnDecl { dv with name }
let levels := dv.levelParams.map .param
let old := .const dv.name levels
let new := .const name levels
let name ← mkFreshUserName <| dv.name.str "eq"
addDecl <|
.thmDecl
{ name
levelParams := dv.levelParams
type := ← mkEq old new
value := ← mkEqRefl old }
Compiler.CSimp.add name .global
