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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.checkValidAutoBoundImplicitName n allowed relaxed = Except.ok false

def Lean.Elab.isValidAutoBoundLevelName (n : 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

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.

instance Lean.Elab.instInhabitedAutoBoundImplicitContext : Inhabited AutoBoundImplicitContext

Equations

• Lean.Elab.instInhabitedAutoBoundImplicitContext = { default := Lean.Elab.instInhabitedAutoBoundImplicitContext.default }

def Lean.Elab.instInhabitedAutoBoundImplicitContext.default : AutoBoundImplicitContext

Equations

• Lean.Elab.instInhabitedAutoBoundImplicitContext.default = { autoImplicitEnabled := default, boundVariables := default }

instance Lean.Elab.instEmptyCollectionAutoBoundImplicitContext : EmptyCollection AutoBoundImplicitContext

Equations

• Lean.Elab.instEmptyCollectionAutoBoundImplicitContext = { emptyCollection := { autoImplicitEnabled := false } }

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.

Equations

• ctx.push x = { autoImplicitEnabled := ctx.autoImplicitEnabled, boundVariables := Lean.PersistentArray.push ctx.boundVariables x }