Basic support for auto bound implicit local names

opaque Lean.Elab.autoImplicit : Lean.Option Bool

opaque Lean.Elab.relaxedAutoImplicit : Lean.Option Bool

Remark: Issue #255 exposed a nasty interaction between macro scopes and auto-bound-implicit names.

local notation "A" => id x
theorem test : A = A := sorry

We used to use n.eraseMacroScopes at isValidAutoBoundImplicitName and isValidAutoBoundLevelName. Thus, in the example above, when A is expanded, a x with a fresh macro scope is created. x+macros-scope is not in scope and is a valid auto-bound implicit name after macro scopes are erased. So, an auto-bound exception would be thrown, and x+macro-scope would be added as a new implicit. When, we try again, a x with a new macro scope is created and this process keeps repeating. Therefore, we do consider identifier with macro scopes anymore.

def Lean.Elab.isValidAutoBoundImplicitName (n : Lake.Name) (relaxed : Bool) : Bool

Equations

• Lean.Elab.isValidAutoBoundImplicitName (Lean.Name.anonymous.str s) relaxed = (decide (s.length > 0) && (relaxed || Lean.Elab.isValidAutoBoundSuffix s))
• Lean.Elab.isValidAutoBoundImplicitName n relaxed = false

def Lean.Elab.isValidAutoBoundLevelName (n : Lake.Name) (relaxed : Bool) : Bool

Equations

• Lean.Elab.isValidAutoBoundLevelName (Lean.Name.anonymous.str s) relaxed = (decide (s.length > 0) && (relaxed || s.front.isLower && Lean.Elab.isValidAutoBoundSuffix s))
• Lean.Elab.isValidAutoBoundLevelName n relaxed = false