Documentation

Lean.Elab.AutoBound

Basic support for auto bound implicit local names #

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.