Name generator for declarations

This module provides functionality to generate a name for a declaration using its binders and its type. This is used to generate names for anonymous instances.

It uses heuristics to generate an informative but terse name given its namespace, supplied binders, and type. It tries to make these relatively unique, and it uses suffixes derived from the module to ensure cross-project uniqueness when the instance doesn't refer to anything defined in the current project.

The name generator can be thought of as a kind of pretty printer, rendering an expression in textual form. The general structure of this generator is

1. Lean.Elab.Command.NameGen.winnowExpr takes an expression and re-uses Expr as a data structure to record the "Syntax"-like structure.
2. Lean.Elab.Command.NameGen.mkBaseNameCore formats the result of that as a string. It actually does a bit more computation than that, since it further removes duplicate expressions, reporting only the first occurrence of each subexpression.

def Lean.Elab.Command.NameGen.mkBaseName (e : Lean.Expr) : Lean.Elab.Command.NameGen.MkNameM✝ String

Given an expression, generates a "base name" for a declaration. The top-level foralls in e are treated as being binders, so use the ...Of... naming convention. The current namespace is used to seed the seen expressions with each prefix of the namespace that's a global constant.

Collects all constants that contribute to the name in the MkInstM state. This can be used to decide whether to further transform the generated name; in particular, this enables checking whether the generated name mentions declarations from the current module or project.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.NameGen.mkBaseNameWithSuffix (pre : String) (type : Lean.Expr) : Lean.MetaM Lean.Name

Uses heuristics to generate an informative but terse base name for a term of the given type, using mkBaseName. Makes use of the current namespace. It tries to make these names relatively unique ecosystem-wide, and it adds suffixes using the current module if the resulting name doesn't refer to anything defined in this module.

If any constant in type has a name with macro scopes, then the result will be a name with fresh macro scopes. While in this case we could skip the naming heuristics, we still want informative names for debugging purposes.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.NameGen.mkBaseNameWithSuffix' (pre : String) (binders : Array Lean.Syntax) (type : Lean.Syntax) : Lean.Elab.TermElabM Lean.Name

Elaborates the binders and type and then uses mkBaseNameWithSuffix to generate a name. Furthermore, uses mkUnusedBaseName on the result.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.mkInstanceName (binders : Array Lean.Syntax) (type : Lean.Syntax) : Lean.Elab.Command.CommandElabM Lean.Name

Generates an instance name for a declaration that has the given binders and type. It tries to make these names relatively unique ecosystem-wide.

Note that this elaborates the binders and the type. This means that when elaborating an instance declaration, we elaborate these twice.