Documentation

Lean.Elab.Term

Saved context for postponed terms and tactics to be executed.

Instances For

    We use synthetic metavariables as placeholders for pending elaboration steps.

    Instances For

      Convert an "extra" optional error message into a message "\n{msg}" (if some msg) and MessageData.nil (if none)

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

        We can optionally associate an error context with a metavariable (see MVarErrorInfo). We have three different kinds of error context.

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

          We can optionally associate an error context with metavariables.

          Instances For
            Equations

            Nested let rec expressions are eagerly lifted by the elaborator. We store the information necessary for performing the lifting here.

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

              State of the TermElabM monad.

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

                Backtrackable state for the TermElabM monad.

                Instances For

                  State of the TacticM monad.

                  Instances For

                    Snapshots are used to implement the save tactic. This tactic caches the state of the system, and allows us to "replay" expensive proofs efficiently. This is only relevant implementing the LSP server.

                    Instances For

                      Key for the cache used to implement the save tactic.

                      Instances For
                        Equations

                        Snapshot after finishing execution of a tactic.

                        Instances For

                          Snapshot just before execution of a tactic.

                          Instances For
                            Equations
                            • Lean.Elab.Tactic.instInhabitedTacticParsedSnapshotData = { default := { toSnapshot := default, stx := default, inner? := default, finished := default, next := default } }
                            • declName? : Option Lake.Name
                            • auxDeclToFullName : Lean.FVarIdMap Lake.Name

                              Map .auxDecl local declarations used to encode recursive declarations to their full-names.

                            • mayPostpone : Bool

                              When mayPostpone == true, an elaboration function may interrupt its execution by throwing Exception.postpone. The function elabTerm catches this exception and creates fresh synthetic metavariable ?m, stores ?m in the list of pending synthetic metavariables, and returns ?m.

                            • errToSorry : Bool

                              When errToSorry is set to true, the method elabTerm catches exceptions and converts them into synthetic sorrys. The implementation of choice nodes and overloaded symbols rely on the fact that when errToSorry is set to false for an elaboration function F, then errToSorry remains false for all elaboration functions invoked by F. That is, it is safe to transition errToSorry from true to false, but we must not set errToSorry to true when it is currently set to false.

                            • autoBoundImplicit : Bool

                              When autoBoundImplicit is set to true, instead of producing an "unknown identifier" error for unbound variables, we generate an internal exception. This exception is caught at elabBinders and elabTypeWithUnboldImplicit. Both methods add implicit declarations for the unbound variable and try again.

                            • autoBoundImplicits : Lean.PArray Lean.Expr
                            • autoBoundImplicitForbidden : Lake.NameBool

                              A name n is only eligible to be an auto implicit name if autoBoundImplicitForbidden n = false. We use this predicate to disallow f to be considered an auto implicit name in a definition such as

                              def f : f → Bool := fun _ => true
                              
                            • sectionVars : Lake.NameMap Lake.Name

                              Map from user name to internal unique name

                            • sectionFVars : Lake.NameMap Lean.Expr

                              Map from internal name to fvar

                            • implicitLambda : Bool

                              Enable/disable implicit lambdas feature.

                            • heedElabAsElim : Bool

                              Heed elab_as_elim attribute.

                            • isNoncomputableSection : Bool

                              Noncomputable sections automatically add the noncomputable modifier to any declaration we cannot generate code for.

                            • ignoreTCFailures : Bool

                              When true we skip TC failures. We use this option when processing patterns.

                            • inPattern : Bool

                              true when elaborating patterns. It affects how we elaborate named holes.

                            • Cache for the save tactic. It is only some in the LSP server.

                            • Snapshot for incremental processing of current tactic, if any.

                              Invariant: if the bundle's old? is set, then the state up to the start of the tactic is unchanged, i.e. reuse is possible.

                            • saveRecAppSyntax : Bool

                              If true, we store in the Expr the Syntax for recursive applications (i.e., applications of free variables tagged with isAuxDecl). We store the Syntax using mkRecAppWithSyntax. We use the Syntax object to produce better error messages at Structural.lean and WF.lean.

                            • holesAsSyntheticOpaque : Bool

                              If holesAsSyntheticOpaque is true, then we mark metavariables associated with _s as syntheticOpaque if 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 => _)

                            Instances For
                              Equations
                              • Lean.Elab.Term.instInhabitedTermElabM = { default := throw default }
                              Equations
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[specialize #[]]

                                  Like Meta.withRestoreOrSaveFull for TermElabM, but also takes a tacSnap? that

                                  • when running act, is set as Context.tacSnap?
                                  • otherwise (i.e. on restore) is used to update the new snapshot promise to the old task's value. This extra restore step is necessary because while reusableResult? can be used to replay any effects on State, Context.tacSnap? is not part of it but changed via an IO side effect, so it needs to be replayed separately.

                                  We use an explicit parameter instead of accessing Context.tacSnap? directly because this prevents withRestoreOrSaveFull and withReader from being used in the wrong order.

                                  Instances For
                                    def Lean.Elab.Term.withReuseContext {m : TypeType u_1} {α : Type} [Monad m] [MonadWithReaderOf Lean.Core.Context m] (stx : Lean.Syntax) (act : m α) :
                                    m α

                                    Incremental elaboration helper. Avoids leakage of data from outside syntax via the monadic context when running act on stx by

                                    • setting stx as the ref and
                                    • deactivating suppressElabErrors if stx is missing-free, which also helps with not hiding useful errors in this part of the input. Note that if stx has missing, this should always be true for the outer syntax as well, so taking the old value of suppressElabErrors into account should not introduce data leakage.

                                    This combinator should always be used when narrowing reuse to a syntax subtree, usually (in the case of tactics, to be generalized) via withNarrowed(Arg)TacticReuse.

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

                                      Manages reuse information for nested tactics by splitting given syntax into an outer and inner part. act is then run on the inner part but with reuse information adjusted as following:

                                      • If the old (from tacSnap?'s SyntaxGuarded.stx) and new (from stx) outer syntax are not identical according to Syntax.eqWithInfo, reuse is disabled.
                                      • Otherwise, the old syntax as stored in tacSnap? is updated to the old inner syntax.
                                      • In any case, withReuseContext is used on the new inner syntax to further prepare the monadic context.

                                      For any tactic that participates in reuse, withNarrowedTacticReuse should be applied to the tactic's syntax and act should be used to do recursive tactic evaluation of nested parts.

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

                                        A variant of withNarrowedTacticReuse that uses stx[argIdx] as the inner syntax and all stx child nodes before that as the outer syntax, i.e. reuse is disabled if there was any change before argIdx.

                                        NOTE: child nodes after argIdx are not tested (which would almost always disable reuse as they are necessarily shifted by changes at argIdx) so it must be ensured that the result of arg does not depend on them (i.e. they should not be inspected beforehand).

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

                                          Disables incremental tactic reuse and reporting for act if cond is true by setting tacSnap? to none. This should be done for tactic blocks that are run multiple times as otherwise the reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is similarly questionable).

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

                                            Disables incremental tactic reuse for act if cond is true.

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

                                              Execute x, save resulting expression and new state. We remove any Info created by x. The info nodes are committed when we execute applyResult. We use observing to implement overloaded notation and decls. We want to save Info nodes for the chosen alternative.

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

                                                Apply the result/exception and state captured with observing. We use this method to implement overloaded notation and symbols.

                                                Equations
                                                Instances For

                                                  Execute 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.

                                                  Equations
                                                  Instances For

                                                    Return the universe level names explicitly provided by the user.

                                                    Equations
                                                    Instances For

                                                      Given a free variable fvar, return its declaration. This function panics if fvar is not a free variable.

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

                                                        Execute x without storing Syntax for recursive applications. See saveRecAppSyntax field at Context.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[implemented_by Lean.Elab.Term.mkTermElabAttributeUnsafe]

                                                          Auxiliary datatype for presenting a Lean lvalue modifier. We represent an unelaborated lvalue as a Syntax (or Expr) and List LVal. Example: a.foo.1 is represented as the Syntax a and the list [LVal.fieldName "foo", LVal.fieldIdx 1].

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

                                                                Return the name of the declaration being elaborated if available.

                                                                Equations
                                                                Instances For

                                                                  Return the list of nested let rec declarations that need to be lifted.

                                                                  Equations
                                                                  Instances For

                                                                    Return the declaration of the given metavariable

                                                                    Equations
                                                                    Instances For

                                                                      Execute withSaveParentDeclInfoContext x with declName? := name. See getDeclName?.

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

                                                                        Update the universe level parameter names.

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

                                                                          Execute x using levelNames as the universe level parameter names. See getLevelNames.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            def Lean.Elab.Term.withAuxDecl {α : Type} (shortDeclName : Lake.Name) (type : Lean.Expr) (declName : Lake.Name) (k : Lean.ExprLean.Elab.TermElabM α) :

                                                                            Declare an auxiliary local declaration shortDeclName : type for elaborating recursive declaration declName, update the mapping auxDeclToFullName, and then execute k.

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

                                                                                Execute x without converting errors (i.e., exceptions) to sorry applications. Recall that when errToSorry = true, the method elabTerm catches exceptions and converts them into sorry applications.

                                                                                Equations
                                                                                • Lean.Elab.Term.withoutErrToSorry = monadMap fun {β : Type} => Lean.Elab.Term.withoutErrToSorryImp
                                                                                Instances For
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For

                                                                                    Execute x without heeding the elab_as_elim attribute. Useful when there is no expected type (so elabAppArgs would fail), but expect that the user wants to use such constants.

                                                                                    Equations
                                                                                    • Lean.Elab.Term.withoutHeedElabAsElim = monadMap fun {β : Type} => Lean.Elab.Term.withoutHeedElabAsElimImp
                                                                                    Instances For

                                                                                      Execute x but discard changes performed at Term.State and Meta.State. Recall that the Environment and 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. The InfoTrees are not discarded, however, and wrapped in InfoTree.Context to store their metavariable context.

                                                                                      Equations
                                                                                      Instances For

                                                                                        Wraps the trees returned from getInfoTrees, if any, in an InfoTree.context node based on the current monadic context and state. This is mainly used to report info trees early via Snapshot.infoTree?. The trees are not removed from the getInfoTrees state as the final info tree of the elaborated command should be complete and not depend on whether parts have been reported early.

                                                                                        As InfoTree.context can have only one child, this function panics if trees contains more than 1 tree. Also, PartialContextInfo.parentDeclCtx is not currently generated as that information is not available in the monadic context and only needed for the final info tree.

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

                                                                                          For testing TermElabM methods. The #eval command will sign the error.

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

                                                                                              Elaborate x with stx on the macro stack

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

                                                                                                Elaborate x with stx on the macro stack and produce macro expansion info

                                                                                                Equations
                                                                                                Instances For

                                                                                                  Add the given metavariable to the list of pending synthetic metavariables. The method synthesizeSyntheticMVars is used to process the metavariables on this list.

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

                                                                                                        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.

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

                                                                                                            Append the argument name (if available) to the message. Remark: if the argument name contains macro scopes we do not append it.

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

                                                                                                              Try to log errors for the unassigned metavariables pendingMVarIds.

                                                                                                              Return 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.

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

                                                                                                                Ensure metavariables registered using registerMVarErrorInfos (and used in the given declaration) have been assigned.

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

                                                                                                                  Execute x without allowing it to postpone elaboration tasks. That is, tryPostpone is a noop.

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

                                                                                                                    Creates syntax for ( <ident> : <type> )

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

                                                                                                                      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.

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

                                                                                                                        Auxiliary method for creating fresh binder names. Do not confuse with the method for creating fresh free/meta variable ids.

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          Auxiliary method for creating a Syntax.ident containing a fresh name. This method is intended for creating fresh binder names. It is just a thin layer on top of mkFreshUserName.

                                                                                                                          Equations
                                                                                                                          Instances For

                                                                                                                            Apply given attributes at a given application time

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                def Lean.Elab.Term.throwTypeMismatchError {α : Type} (header? : Option String) (expectedType : Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) (f? : optParam (Option Lean.Expr) none) (_extraMsg? : optParam (Option Lean.MessageData) none) :
                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For

                                                                                                                                    Return true if e contains a pending metavariable. Remark: it also visits let-declarations.

                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      def Lean.Elab.Term.synthesizeInstMVarCore (instMVar : Lean.MVarId) (maxResultSize? : optParam (Option Nat) none) (extraErrorMsg? : optParam (Option Lean.MessageData) none) :

                                                                                                                                      Try to synthesize metavariable using type class resolution. This method assumes the local context and local instances of instMVar coincide with the current local context and local instances. Return true if the instance was synthesized successfully, and false if the instance contains unassigned metavariables that are blocking the type class resolution procedure. Throw an exception if resolution or assignment irrevocably fails.

                                                                                                                                      If extraErrorMsg? is not none, it contains additional information that should be attached to type class synthesis failures.

                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For
                                                                                                                                        def Lean.Elab.Term.mkCoe (expectedType : Lean.Expr) (e : Lean.Expr) (f? : optParam (Option Lean.Expr) none) (errorMsgHeader? : optParam (Option String) none) :
                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For

                                                                                                                                          If expectedType? is some t, then ensures t and eType are definitionally equal by inserting a coercion if necessary.

                                                                                                                                          Argument f? is used only for generating error messages when inserting coercions fails.

                                                                                                                                          Equations
                                                                                                                                          Instances For

                                                                                                                                            Log the given exception, and create a synthetic sorry for representing the failed elaboration step with exception ex.

                                                                                                                                            Equations
                                                                                                                                            Instances For

                                                                                                                                              If mayPostpone == true, throw Expection.postpone.

                                                                                                                                              Equations
                                                                                                                                              Instances For

                                                                                                                                                Return true if e reduces (by unfolding only [reducible] declarations) to ?m ...

                                                                                                                                                Equations
                                                                                                                                                Instances For

                                                                                                                                                  If mayPostpone == true and e's head is a metavariable, throw Exception.postpone.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For

                                                                                                                                                    Throws Exception.postpone, if expectedType? contains unassigned metavariables. It is a noop if mayPostpone == false.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For

                                                                                                                                                      Throws Exception.postpone, if expectedType? contains unassigned metavariables. If mayPostpone == false, it throws error msg.

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

                                                                                                                                                          Save relevant context for term elaboration postponement.

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

                                                                                                                                                            Execute x with the context saved using saveContext.

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

                                                                                                                                                                Create an auxiliary annotation to make sure we create an Info even if e is a metavariable. See mkTermInfo.

                                                                                                                                                                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 metavariable ?n. The elaborator for

                                                                                                                                                                let_mvar% ?m := b; wait_if_type_mvar% ?m; body
                                                                                                                                                                

                                                                                                                                                                returns 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.

                                                                                                                                                                Equations
                                                                                                                                                                Instances For

                                                                                                                                                                  Return 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 InfoTree.

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

                                                                                                                                                                      Pushes a new leaf node to the info tree associating the expression e to the syntax stx. As a result, when the user hovers over stx they will see the type of e, and if e is a constant they will see the constant's doc string.

                                                                                                                                                                      • expectedType?: the expected type of e at the point of elaboration, if available
                                                                                                                                                                      • lctx?: the local context in which to interpret e (otherwise it will use ← getLCtx)
                                                                                                                                                                      • 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 addTermInfo is 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.)
                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For
                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For

                                                                                                                                                                            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. When stx is elaborated, new info nodes are created and attached to the new hole id in the info tree.

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

                                                                                                                                                                              Block usage of implicit lambdas if stx is @f or @f arg1 ... or fun with an implicit binder annotation.

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

                                                                                                                                                                                      Return true iff stx is a Syntax.ident, and it is a local variable.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For

                                                                                                                                                                                        Store in the InfoTree that e is a "dot"-completion target. stx should cover the entire term.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          def Lean.Elab.Term.elabTerm (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (catchExPostpone : optParam Bool true) (implicitLambda : optParam Bool true) :

                                                                                                                                                                                          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 SyntaxNodeKind to TermElab methods. 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 Exception.error and errToSorry == true, the error is logged and a synthetic sorry expression is returned. If the elaboration throws Exception.postpone and catchExPostpone == true, a new synthetic metavariable of kind SyntheticMVarKind.postponed is created, registered, and returned. The option catchExPostpone == false is used to implement resumeElabTerm to prevent the creation of another synthetic metavariable when resuming the elaboration.

                                                                                                                                                                                          If 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.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            def Lean.Elab.Term.elabTermEnsuringType (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (catchExPostpone : optParam Bool true) (implicitLambda : optParam Bool true) (errorMsgHeader? : optParam (Option String) none) :

                                                                                                                                                                                            Similar to Lean.Elab.Term.elabTerm, but ensures that the type of the elaborated term is expectedType? by inserting coercions if necessary.

                                                                                                                                                                                            If errToSorry is true, then if coercion insertion fails, this function returns sorry and logs the error. Otherwise, it throws the error.

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

                                                                                                                                                                                              Execute x and return some if no new errors were recorded or exceptions were thrown. Otherwise, return none.

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

                                                                                                                                                                                                Adapt a syntax transformation to a regular, term-producing elaborator.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  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 type), register metavariable as a pending one.

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

                                                                                                                                                                                                    Make sure e is a type by inferring its type and making sure it is an Expr.sort or is unifiable with Expr.sort, or can be coerced into one.

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

                                                                                                                                                                                                      Elaborate stx and ensure result is a type.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                        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.

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

                                                                                                                                                                                                              Collect unassigned metavariables in type that are not already in init and not satisfying except.

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

                                                                                                                                                                                                                Return autoBoundImplicits ++ xs This method throws an error if a variable in autoBoundImplicits depends on some x in xs. The autoBoundImplicits may contain free variables created by the auto-implicit feature, and unassigned free variables. It avoids the hack used at autoBoundImplicitsOld.

                                                                                                                                                                                                                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 k.

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

                                                                                                                                                                                                                    Similar to autoBoundImplicits, but immediately if the resulting array of expressions contains metavariables, it immediately uses mkForallFVars + forallBoundedTelescope to convert them into free variables. The type type is modified during the process if type depends on xs. We use this method to simplify the conversion of code using autoBoundImplicitsOld to autoBoundImplicits.

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

                                                                                                                                                                                                                        Return true if mvarId is an auxiliary metavariable created for compiling let rec or it is delayed assigned to one.

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          def Lean.Elab.Term.mkConst (constName : Lake.Name) (explicitLevels : optParam (List Lean.Level) []) (checkDeprecated : optParam Bool true) :

                                                                                                                                                                                                                          Create an Expr.const using the given name and explicit levels. Remark: fresh universe metavariables are created if the constant has more universe parameters than explicitLevels.

                                                                                                                                                                                                                          If checkDeprecated := true, then Linter.checkDeprecated is invoked.

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

                                                                                                                                                                                                                                Similar to resolveName, but creates identifiers for the main part and each projection with position information derived from ident. Example: Assume resolveName v.head.bla.boo produces (v.head, ["bla", "boo"]), then this method produces (v.head, id, [f₁, f₂]) where id is an identifier for v.head, and f₁ and f₂ are identifiers for fields "bla" and "boo".

                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  def Lean.Elab.Term.TermElabM.run {α : Type} (x : Lean.Elab.TermElabM α) (ctx : optParam Lean.Elab.Term.Context { declName? := none, auxDeclToFullName := , macroStack := [], mayPostpone := true, errToSorry := true, autoBoundImplicit := false, autoBoundImplicits := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, autoBoundImplicitForbidden := fun (x : Lake.Name) => false, sectionVars := , sectionFVars := , implicitLambda := true, heedElabAsElim := true, isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false, tacticCache? := none, tacSnap? := none, saveRecAppSyntax := true, holesAsSyntheticOpaque := false }) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := , pendingMVars := , mvarErrorInfos := [], mvarArgNames := , letRecsToLift := [] }) :
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                    def Lean.Elab.Term.TermElabM.run' {α : Type} (x : Lean.Elab.TermElabM α) (ctx : optParam Lean.Elab.Term.Context { declName? := none, auxDeclToFullName := , macroStack := [], mayPostpone := true, errToSorry := true, autoBoundImplicit := false, autoBoundImplicits := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, autoBoundImplicitForbidden := fun (x : Lake.Name) => false, sectionVars := , sectionFVars := , implicitLambda := true, heedElabAsElim := true, isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false, tacticCache? := none, tacSnap? := none, saveRecAppSyntax := true, holesAsSyntheticOpaque := false }) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := , pendingMVars := , mvarErrorInfos := [], mvarArgNames := , letRecsToLift := [] }) :
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • x.toIO ctxCore sCore ctxMeta sMeta ctx s = do let __discr(x.run ctx s).toIO ctxCore sCore ctxMeta sMeta match __discr with | ((a, s), sCore, sMeta) => pure (a, sCore, sMeta, s)
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.

                                                                                                                                                                                                                                        Execute x and then tries to solve pending universe constraints. Note that, stuck constraints will not be discarded.

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

                                                                                                                                                                                                                                            Helper function for "embedding" an Expr in Syntax. It creates a named hole ?m and immediately assigns e to it. Examples:

                                                                                                                                                                                                                                            let e := mkConst ``Nat.zero
                                                                                                                                                                                                                                            `(Nat.succ $(← exprToSyntax e))
                                                                                                                                                                                                                                            
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                Checks whether a declaration is annotated with [builtin_incremental] or [incremental].

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