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 don't consider identifier with macro scopes anymore.

An .error value should be treated as a false—this is not a valid auto-bound implicit name— but it contains additional notes (above and beyond Unknown identifier) to attach to an error message.

def Lean.Elab.checkValidAutoBoundImplicitName (n : Name) (allowed relaxed : Bool) : Except MessageData Bool

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

structure Lean.Elab.AutoBoundImplicitContext : Type

Tracks extra context needed within the scope of Lean.Elab.Term.withAutoBoundImplicit

• autoImplicitEnabled : Bool

  This always matches the autoImplicit option; it is duplicated here in order to support the behavior of the deprecated Lean.Elab.Term.Context.autoImplicit method.

• boundVariables : PArray Expr

  Tracks a working set of variables that the auto-binding process currently anticipates adding implicit binding for.

@[implicit_reducible]

instance Lean.Elab.instInhabitedAutoBoundImplicitContext : Inhabited AutoBoundImplicitContext

def Lean.Elab.instInhabitedAutoBoundImplicitContext.default : AutoBoundImplicitContext

@[implicit_reducible]

instance Lean.Elab.instEmptyCollectionAutoBoundImplicitContext : EmptyCollection AutoBoundImplicitContext

def Lean.Elab.AutoBoundImplicitContext.push (ctx : AutoBoundImplicitContext) (x : Expr) : AutoBoundImplicitContext

Pushes a new variable onto the autoImplicit context, indicating that it needs to be bound as an implicit parameter.