- typeClass: Lean.Elab.Term.SyntheticMVarKind
Use typeclass resolution to synthesize value for metavariable.
- coe: Option String → Lean.Expr → Lean.Expr → Option Lean.Expr → Lean.Elab.Term.SyntheticMVarKind
Use coercion to synthesize value for the metavariable. if
some f, we produce an application type mismatch error message. Otherwise, if
some header, we generate the error
(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)Otherwise, we generate the error
("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)
- tactic: Lean.Syntax → Lean.Elab.Term.SavedContext → Lean.Elab.Term.SyntheticMVarKind
Use tactic to synthesize value for metavariable.
- postponed: Lean.Elab.Term.SavedContext → Lean.Elab.Term.SyntheticMVarKind
Metavariable represents a hole whose elaboration has been postponed.
We use synthetic metavariables as placeholders for pending elaboration steps.
- implicitArg: Lean.Expr → Lean.Elab.Term.MVarErrorKind
Metavariable for implicit arguments.
ctxis the parent application.
- hole: Lean.Elab.Term.MVarErrorKind
Metavariable for explicit holes provided by the user (e.g.,
- custom: Lean.MessageData → Lean.Elab.Term.MVarErrorKind
msgDatastores the additional error messages.
We can optionally associate an error context with a metavariable (see
We have three different kinds of error context.
- ref : Lean.Syntax
- fvarId : Lean.FVarId
- shortDeclName : Lake.Name
- declName : Lake.Name
- lctx : Lean.LocalContext
- localInstances : Lean.LocalInstances
- type : Lean.Expr
- val : Lean.Expr
let rec expressions are eagerly lifted by the elaborator.
We store the information necessary for performing the lifting here.
State of the
- core : Lean.Core.State
- meta : Lean.Meta.State
- term : Lean.Elab.Term.State
- tactic : Lean.Elab.Tactic.State
- stx : Lean.Syntax
Snapshots are used to implement the
This tactic caches the state of the system, and allows us to "replay"
expensive proofs efficiently. This is only relevant implementing the
.auxDecllocal declarations used to encode recursive declarations to their full-names.
- macroStack : Lean.Elab.MacroStack
- mayPostpone : Bool
- errToSorry : Bool
errToSorryis set to true, the method
elabTermcatches exceptions and converts them into synthetic
sorrys. The implementation of choice nodes and overloaded symbols rely on the fact that when
errToSorryis set to false for an elaboration function
falsefor all elaboration functions invoked by
F. That is, it is safe to transition
false, but we must not set
truewhen it is currently set to
- autoBoundImplicit : Bool
autoBoundImplicitis set to true, instead of producing an "unknown identifier" error for unbound variables, we generate an internal exception. This exception is caught at
elabTypeWithUnboldImplicit. Both methods add implicit declarations for the unbound variable and try again.
Map from user name to internal unique name
Map from internal name to fvar
- implicitLambda : Bool
Enable/disable implicit lambdas feature.
- isNoncomputableSection : Bool
Noncomputable sections automatically add the
noncomputablemodifier to any declaration we cannot generate code for.
- ignoreTCFailures : Bool
truewe skip TC failures. We use this option when processing patterns.
- inPattern : Bool
truewhen elaborating patterns. It affects how we elaborate named holes.
Cache for the
savetactic. It is only
somein the LSP server.
- saveRecAppSyntax : Bool
true, we store in the
Syntaxfor recursive applications (i.e., applications of free variables tagged with
isAuxDecl). We store the
mkRecAppWithSyntax. We use the
Syntaxobject to produce better error messages at
- holesAsSyntheticOpaque : Bool
true, then we mark metavariables associated with
synthethicOpaqueif they do not occur in patterns. This option is useful when elaborating terms in tactics such as
refine'where we want holes there to become new goals. See issue #1681, we have `refine' (fun x => _)
x, save resulting expression and new state.
We remove any
Info created by
The info nodes are committed when we execute
observing to implement overloaded notation and decls.
We want to save
Info nodes for the chosen alternative.
x, but keep state modifications only if
x did not postpone.
This method is useful to implement elaboration functions that cannot decide whether
they need to postpone or not without updating the state.
x but discard changes performed at
Recall that the
InfoState are at
Core.State. Thus, any updates to it will
be preserved. This method is useful for performing computations where all
metavariable must be resolved or discarded.
InfoTrees are not discarded, however, and wrapped in
to store their metavariable context.
- fieldIdx: Lean.Syntax → Nat → Lean.Elab.Term.LVal
- fieldName: Lean.Syntax → String → Option Lake.Name → Lean.Syntax → Lean.Elab.Term.LVal
suffix?is for producing better error messages because
x.ymay be a field access or a hierarchical/composite name.
refis the syntax object representing the field.
targetStxis the target object being accessed.
Auxiliary datatype for presenting a Lean lvalue modifier.
We represent an unelaborated lvalue as a
a.foo.1 is represented as the
a and the list
[LVal.fieldName "foo", LVal.fieldIdx 1].
Add the given metavariable to the list of pending synthetic metavariables.
synthesizeSyntheticMVars is used to process the metavariables on this list.
Auxiliary method for reporting errors of the form "... contains metavariables ...".
This kind of error is thrown, for example, at
Match.lean where elaboration
cannot continue if there are metavariables in patterns.
We only want to log it if we haven't logged any errors so far.
mvarErrorInfo argument name (if available) to the message.
Remark: if the argument name contains macro scopes we do not append it.
Try to log errors for the unassigned metavariables
true if there were "unfilled holes", and we should "abort" declaration.
TODO: try to fill "all" holes using synthetic "sorry's"
Remark: We only log the "unfilled holes" as new errors if no error has been logged so far.
Convert unassigned universe level metavariables into parameters.
The new parameter names are fresh names of the form
u_i with regard to
ctx.levelNames, which is updated with the new names.
Auxiliary method for creating a
a fresh name. This method is intended for creating fresh binder names.
It is just a thin layer on top of
Try to synthesize metavariable using type class resolution.
This method assumes the local context and local instances of
with the current local context and local instances.
true if the instance was synthesized successfully, and
the instance contains unassigned metavariables that are blocking the type class
resolution procedure. Throw an exception if resolution or assignment irrevocably fails.
some t, then ensure
eType are definitionally equal.
If they are not, then try coercions.
f? is used only for generating error messages.
Create an auxiliary annotation to make sure we create an
Info even if
e is a metavariable.
We use this function because some elaboration functions elaborate subterms that may not be immediately part of the resulting term. Example:
let_mvar% ?m := b; wait_if_type_mvar% ?m; body
If the type of
b is not known, then
wait_if_type_mvar% ?m; body is postponed and just returns a fresh
?n. The elaborator for
let_mvar% ?m := b; wait_if_type_mvar% ?m; body
mkSaveInfoAnnotation ?n to make sure the info nodes created when elaborating
b are "saved".
This is a bit hackish, but elaborators like
let_mvar% are rare.
some mvarId if
e corresponds to a hole that is going to be filled "later" by executing a tactic or resuming elaboration.
We do not save
ofTermInfo for this kind of node in the
Pushes a new leaf node to the info tree associating the expression
e to the syntax
As a result, when the user hovers over
stx they will see the type of
e, and if
is a constant they will see the constant's doc string.
expectedType?: the expected type of
eat the point of elaboration, if available
lctx?: the local context in which to interpret
e(otherwise it will use
elaborator: a declaration name used as an alternative target for go-to-definition
isBinder: if true, this will be treated as defining
e(which should be a local constant) for the purpose of go-to-definition on local variables
force: In patterns, the effect of
addTermInfois usually suppressed and replaced by a
patternWithRef?annotation which will be turned into a term info on the post-match-elaboration expression. This flag overrides that behavior and adds the term info immediately. (See https://github.com/leanprover/lean4/pull/1664.)
Postpone the elaboration of
stx, return a metavariable that acts as a placeholder, and
ensures the info tree is updated and a hole id is introduced.
stx is elaborated, new info nodes are created and attached to the new hole id in the info tree.
- One or more equations did not get rendered due to their size.
Main function for elaborating terms.
It extracts the elaboration methods from the environment using the node kind.
Recall that the environment has a mapping from
It creates a fresh macro scope for executing the elaboration method.
All unlogged trace messages produced by the elaboration method are logged using
the position information at
stx. If the elaboration method throws an
errToSorry == true,
the error is logged and a synthetic sorry expression is returned.
If the elaboration throws
catchExPostpone == true,
a new synthetic metavariable of kind
SyntheticMVarKind.postponed is created, registered,
catchExPostpone == false is used to implement
to prevent the creation of another synthetic metavariable when resuming the elaboration.
implicitLambda == false, then disable implicit lambdas feature for the given syntax, but not for its subterms.
We use this flag to implement, for example, the
@ modifier. If
Context.implicitLambda == false, then this parameter has no effect.
Create a new metavariable with the given type, and try to synthesize it.
If type class resolution cannot be executed (e.g., it is stuck because of metavariables in
register metavariable as a pending one.
Enable auto-bound implicits, and execute
k while catching auto bound implicit exceptions. When an exception is caught,
a new local declaration is created, registered, and
k is tried to be executed again.
Collect unassigned metavariables in
type that are not already in
init and not satisfying
autoBoundImplicits ++ xs
This method throws an error if a variable in
autoBoundImplicits depends on some
autoBoundImplicits may contain free variables created by the auto-implicit feature, and unassigned free variables.
It avoids the hack used at
Remark: we cannot simply replace every occurrence of
addAutoBoundImplicitsOld with this one because a particular
use-case may not be able to handle the metavariables in the array being given to
autoBoundImplicits, but immediately if the resulting array of expressions contains metavariables,
it immediately uses
forallBoundedTelescope to convert them into free variables.
type is modified during the process if type depends on
We use this method to simplify the conversion of code using
Expr.const using the given name and explicit levels.
Remark: fresh universe metavariables are created if the constant has more universe
resolveName, but creates identifiers for the main part and each projection with position information derived from
Example: Assume resolveName
(v.head, ["bla", "boo"]), then this method produces
(v.head, id, [f₁, f₂]) where
id is an identifier for
f₂ are identifiers for fields