Helper functions for creating auxiliary names used in (old) compiler passes.

def Lean.Compiler.mkEagerLambdaLiftingName (n : Name) (idx : Nat) : Name

def Lean.Compiler.isEagerLambdaLiftingName : Name → Bool

def Lean.Compiler.getDeclNamesForCodeGen : Declaration → Array Name

Return the name of new definitions in the a given declaration. Here we consider only declarations we generate code for. We use this definition to implement add_and_compile.

def Lean.Compiler.checkIsDefinition (env : Environment) (n : Name) : Except String Unit

def Lean.Compiler.mkUnsafeRecName (declName : Name) : Name

We generate auxiliary unsafe definitions for regular recursive definitions. The auxiliary unsafe definition has a clear runtime cost execution model. This function returns the auxiliary unsafe definition name for the given name.

def Lean.Compiler.isUnsafeRecName? : Name → Option Name

Return some _ if the given name was created using mkUnsafeRecName