auto bound implicit args are not limited to single letters

[medovina]

The section Auto Bound Implicit Arguments (in chapter 6 Interacting with Lean) says

When Lean processes the header of a declaration, any unbound identifier is automatically added as an implicit argument if it is a single lower case or greek letter.

However (at least in the current version 4.5.0) this feature does not seem to be limited to single letters. For example:

def foo (x : abc) := x

#check foo

produces

foo.{u_1} {abc : Sort u_1} (x : abc) : abc

So presumably this documentation needs to be updated (unless this is actually considered to be a bug in Lean).

[david-christiansen]

You're right - this is a mistake in the document. Thanks!