RFC: Lean.Name.isUserName

Proposal

There's a few places in Std and Mathlib where there is a desire to filter out auto-generated and other stable names (e.g., leanprover/std4#347 and leanprover/std4#355).

I think this notion could get upstreamed in the hopes that will ensure tactics use a consistent predicate. The predicate I want is already in a test case, but could get moved to Lean/Data/Name.lean:

Hear's the addition I would propose.

/--
Return true if `declName` is a auxillary definition created by elaborator.
-/
def isAuxName : Name → Bool
| .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s
| _ => false

/--
Return true if the name is a user facing name.

This returns false for names that are internal, numerical or appear auxillary created.
-/
def isUserName (declName : Name) : Bool :=
  declName.isStr
  && !declName.isAuxName
  && !declName.isInternal

Community Feedback

I haven't done this, but it's hopefully just moving a definition.

Impact

The potential impact is better consistency of ignoring definitions across tactics that want to show user facing names.

Start with the existing predicate in tests/lean/run/printDecls.lean, then inspect Lean/Data/Name.lean as the proposed destination. Compare the current test behavior with the RFC's isAuxName and isUserName proposal; done means the intended public name-filtering API is placed and its behavior is covered consistently.