The variable? command

This defines a command like variable that automatically adds all missing typeclass arguments. For example, variable? [Module R M] is the same as variable [Semiring R] [AddCommMonoid M] [Module R M], though if any of these three instance arguments can be inferred from previous variables then they will be omitted.

An inherent limitation with this command is that variables are recorded in the scope as syntax. This means that variable? needs to pretty print the expressions we get from typeclass synthesis errors, and these might fail to round trip.

opaque Mathlib.Command.Variable.variable?.maxSteps : Lean.Option Nat

opaque Mathlib.Command.Variable.variable?.checkRedundant : Lean.Option Bool

def Mathlib.Command.Variable.bracketedBinderType : Lean.Syntax → Option Lean.Term

Get the type out of a bracketed binder.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Command.Variable.variable? : Lean.ParserDescr

The variable? command has the same syntax as variable, but it will auto-insert missing instance arguments wherever they are needed. It does not add variables that can already be deduced from others in the current context. By default the command checks that variables aren't implied by earlier ones, but it does not check that earlier variables aren't implied by later ones. Unlike variable, the variable? command does not support changing variable binder types.

The variable? command will give a suggestion to replace itself with a command of the form variable? ...binders... => ...binders.... The binders after the => are the completed list of binders. When this => clause is present, the command verifies that the expanded binders match the post-=> binders. The purpose of this is to help keep code that uses variable? resilient against changes to the typeclass hierarchy, at least in the sense that this additional information can be used to debug issues that might arise. One can also replace variable? ...binders... => with variable.

The core algorithm is to try elaborating binders one at a time, and whenever there is a typeclass instance inference failure, it synthesizes binder syntax for it and adds it to the list of binders and tries again, recursively. There are no guarantees that this process gives the "correct" list of binders.

Structures tagged with the variable_alias attribute can serve as aliases for a collection of typeclasses. For example, given

@[variable_alias]
structure VectorSpace (k V : Type*) [Field k] [AddCommGroup V] [Module k V]

then variable? [VectorSpace k V] is equivalent to variable {k V : Type*} [Field k] [AddCommGroup V] [Module k V], assuming that there are no pre-existing instances on k and V. Note that this is not a simple replacement: it only adds instances not inferrable from others in the current scope.

A word of warning: the core algorithm depends on pretty printing, so if terms that appear in binders do not round trip, this algorithm can fail. That said, it has some support for quantified binders such as [∀ i, F i].

Equations

• One or more equations did not get rendered due to their size.

opaque Mathlib.Command.Variable.variableAliasAttr : Lean.TagAttribute

Attribute to record aliases for the variable? command. Aliases are structures that have no fields, and additional typeclasses are recorded as arguments to the structure.

Example:

@[variable_alias]
structure VectorSpace (k V : Type*)
  [Field k] [AddCommGroup V] [Module k V]

Then variable? [VectorSpace k V] ensures that these three typeclasses are present in the current scope. Notice that it's looking at the arguments to the VectorSpace type constructor. You should not have any fields in variable_alias structures.

Notice that VectorSpace is not a class; the variable? command allows non-classes with the variable_alias attribute to use instance binders.

def Mathlib.Command.Variable.pendingActionableSynthMVar (binder : Lean.TSyntax `Lean.Parser.Term.bracketedBinder) : Lean.Elab.TermElabM (Option Lean.MVarId)

Find a synthetic typeclass metavariable with no expr metavariables in its type.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Command.Variable.getSubproblem (binder : Lean.TSyntax `Lean.Parser.Term.bracketedBinder) (ty : Lean.Term) : Lean.Elab.TermElabM (Option (Lean.MessageData × Lean.TSyntax `Lean.Parser.Term.bracketedBinder))

Try elaborating ty. Returns none if it doesn't need any additional typeclasses, or it returns a new binder that needs to come first. Does not add info unless it throws an exception.

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Command.Variable.completeBinders' (maxSteps : Nat) (gas : Nat) (checkRedundant : Bool) (binders : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) (toOmit : Array Bool) (i : Nat) : Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder × Array Bool)

Tries elaborating binders, inserting new binders whenever typeclass inference fails. i is the index of the next binder that needs to be checked.

The toOmit array keeps track of which binders should be removed at the end, in particular the variable_alias binders and any redundant binders.

def Mathlib.Command.Variable.completeBinders'.isVariableAlias (type : Lean.Expr) : Lean.MetaM Bool

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Command.Variable.completeBinders (maxSteps : Nat) (checkRedundant : Bool) (binders : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) : Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder × Array Bool)

Equations

• Mathlib.Command.Variable.completeBinders maxSteps checkRedundant binders = Mathlib.Command.Variable.completeBinders' maxSteps maxSteps checkRedundant binders #[] 0

def Mathlib.Command.Variable.cleanBinders (binders : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder

Strip off whitespace and comments.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Command.Variable.elabVariables : Lean.Elab.Command.CommandElab

The variable? command has the same syntax as variable, but it will auto-insert missing instance arguments wherever they are needed. It does not add variables that can already be deduced from others in the current context. By default the command checks that variables aren't implied by earlier ones, but it does not check that earlier variables aren't implied by later ones. Unlike variable, the variable? command does not support changing variable binder types.

The variable? command will give a suggestion to replace itself with a command of the form variable? ...binders... => ...binders.... The binders after the => are the completed list of binders. When this => clause is present, the command verifies that the expanded binders match the post-=> binders. The purpose of this is to help keep code that uses variable? resilient against changes to the typeclass hierarchy, at least in the sense that this additional information can be used to debug issues that might arise. One can also replace variable? ...binders... => with variable.

The core algorithm is to try elaborating binders one at a time, and whenever there is a typeclass instance inference failure, it synthesizes binder syntax for it and adds it to the list of binders and tries again, recursively. There are no guarantees that this process gives the "correct" list of binders.

Structures tagged with the variable_alias attribute can serve as aliases for a collection of typeclasses. For example, given

@[variable_alias]
structure VectorSpace (k V : Type*) [Field k] [AddCommGroup V] [Module k V]

then variable? [VectorSpace k V] is equivalent to variable {k V : Type*} [Field k] [AddCommGroup V] [Module k V], assuming that there are no pre-existing instances on k and V. Note that this is not a simple replacement: it only adds instances not inferrable from others in the current scope.

A word of warning: the core algorithm depends on pretty printing, so if terms that appear in binders do not round trip, this algorithm can fail. That said, it has some support for quantified binders such as [∀ i, F i].

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Command.Variable.elabVariables.extendScope (binders : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) : Lean.Elab.Command.CommandElabM Unit

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Command.Variable.elabVariables.process (stx : Lean.Syntax) (checkRedundant : Bool) (binders : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) (expectedBinders? : Option (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder)) : Lean.Elab.Command.CommandElabM Unit

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Command.Variable.ignorevariable? : Lean.Linter.IgnoreFunction

Hint for the unused variables linter. Copies the one for variable.

Equations

• One or more equations did not get rendered due to their size.