Inconsistent Behavior: User Declaration with Leading Underscore Allowed Despite Documentation

Description

There appears to be an inconsistency between the Lean documentation and its actual behavior regarding user declarations with names starting with an underscore (_).

/-- The frontend does not allow user declarations to start with `_` in any of its parts.
   We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
def isInternal : Name → Bool
  | str p s => s.get 0 == '_' || isInternal p
  | num p _ => isInternal p
  | _       => false

Example

def _inside := 0
#eval ``_inside |>.isInternal

In this case, _inside is successfully declared, and isInternal correctly returns true, indicating that the name starts with an underscore.

Additional Information

This issue raises questions about whether the documentation is outdated or if there is a bug in the frontend allowing names with leading underscores. Clarification on this behavior would be helpful for users to understand the intended constraints on naming.

Environment

• Lean version: 4.8.0, 4.10.0-rc2 and more

Related issues

• https://github.com/leanprover/lean4/issues/2850

The difference between the two is that this issue attempts to determine an internal naming style supported by Lean.Elab, i.e.

The frontend does not allow user declarations to start with *** in any of its parts.

Unless another issue can be solved in this way:

I still think we should have some kind of explicit @[automatically_generated] attribute (this is what rust does BTW) to standardize this rather than using underscores, because sometimes autogenerated definitions are also intended for use by users. —— digama0

Start by comparing the documented isInternal rule with the _inside example across Lean 4.8.0 and 4.10.0-rc2. Determine whether frontend rejection or the documentation reflects the intended naming behavior, considering related issue #2850 and the proposed automatically_generated attribute. Done means the supported behavior and naming guidance are resolved and documented.