Documentation

Lean.Elab.InfoTree.Main

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

      Merges the inner partial context into the outer context s.t. fields of the inner context overwrite fields of the outer context. Panics if the invariant described in the documentation for PartialContextInfo is violated.

      When traversing an InfoTree, this function should be used to combine the context of outer nodes with the partial context of their subtrees. This ensures that the traversal has the context from the inner node to the root node of the InfoTree available, with partial contexts of inner nodes taking priority over contexts of outer nodes.

      Equations
      Instances For
        Equations
        Instances For

          Obtains the LocalContext from this CompletionInfo if available and yields an empty context otherwise.

          Equations
          Instances For
            Equations
            Instances For

              Instantiate the holes on the given tree with the assignment table. (analogous to instantiating the metavariables in an expression)

              Embeds a CoreM action in IO by supplying the information stored in info.

              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
                  • info.toPPContext lctx = { env := info.env, mctx := info.mctx, lctx := lctx, opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls }
                  Instances For
                    Equations
                    • info.ppSyntax lctx stx = Lean.ppTerm (info.toPPContext lctx) { raw := stx }
                    Instances For
                      Equations
                      • info.runMetaM ctx x = ctx.runMetaM info.lctx x
                      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
                              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
                                      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
                                            Equations
                                            Instances For

                                              Helper function for propagating the tactic metavariable context to its children nodes. We need this function because we preserve TacticInfo nodes during backtracking and their children. Moreover, we backtrack the metavariable context to undo metavariable assignments. TacticInfo nodes save the metavariable context before/after the tactic application, and can be pretty printed without any extra information. This is not the case for TermInfo nodes. Without this function, the formatting method would often fail when processing TermInfo nodes that are children of TacticInfo nodes that have been preserved during backtracking. Saving the metavariable context at TermInfo nodes is also not a good option because at TermInfo creation time, the metavariable context often miss information, e.g., a TC problem has not been resolved, a postponed subterm has not been elaborated, etc.

                                              See Term.SavedState.restore.

                                              Equations
                                              Instances For

                                                Returns the current array of InfoTrees and resets it to an empty array.

                                                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

                                                        This does the same job as realizeGlobalConstNoOverload; resolving an identifier syntax to a unique fully resolved name or throwing if there are ambiguities. But also adds this resolved name to the infotree. This means that when you hover over a name in the sourcefile you will see the fully resolved name in the hover info.

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

                                                          Similar to realizeGlobalConstNoOverloadWithInfo, except if there are multiple name resolutions then it returns them as a list.

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

                                                            Similar to realizeGlobalName, but it also adds the resolved name to the info tree.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              def Lean.Elab.withInfoContext' {m : TypeType} [Monad m] [Lean.Elab.MonadInfoTree m] {α : Type} [MonadFinally m] (x : m α) (mkInfo : αm (Lean.Elab.Info Lean.MVarId)) :
                                                              m α

                                                              Use this to descend a node on the infotree that is being built.

                                                              It saves the current list of trees t₀ and resets it and then runs x >>= mkInfo, producing either an i : Info or a hole id. Running x >>= mkInfo will modify the trees state and produce a new list of trees t₁. In the i : Info case, t₁ become the children of a node node i t₁ that is appended to t₀.

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

                                                                Saves the current list of trees t₀, runs x to produce a new tree list t₁ and runs mkInfoTree t₁ to get n : InfoTree and then restores the trees to be t₀ ++ [n].

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[inline]
                                                                  def Lean.Elab.withInfoContext {m : TypeType} [Monad m] [Lean.Elab.MonadInfoTree m] {α : Type} [MonadFinally m] (x : m α) (mkInfo : m Lean.Elab.Info) :
                                                                  m α

                                                                  Run x as a new child infotree node with header given by mkInfo.

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

                                                                    Resets the trees state t₀, runs x to produce a new trees state t₁ and sets the state to be t₀ ++ (InfoTree.context (PartialContextInfo.commandCtx Γ) <$> t₁) where Γ is the context derived from the monad state.

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

                                                                      Resets the trees state t₀, runs x to produce a new trees state t₁ and sets the state to be t₀ ++ (InfoTree.context (PartialContextInfo.parentDeclCtx Γ) <$> t₁) where Γ is the parent decl name provided by MonadParentDecl m.

                                                                      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
                                                                            def Lean.Elab.withMacroExpansionInfo {m : TypeType} {α : Type} [MonadFinally m] [Monad m] [Lean.Elab.MonadInfoTree m] [Lean.MonadLCtx m] (stx : Lean.Syntax) (output : Lean.Syntax) (x : m α) :
                                                                            m α
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              @[inline]
                                                                              def Lean.Elab.withInfoHole {m : TypeType} {α : Type} [MonadFinally m] [Monad m] [Lean.Elab.MonadInfoTree m] (mvarId : Lean.MVarId) (x : m α) :
                                                                              m α
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                Equations
                                                                                Instances For
                                                                                  def Lean.Elab.withEnableInfoTree {m : TypeType} {α : Type} [Monad m] [Lean.Elab.MonadInfoTree m] [MonadFinally m] (flag : Bool) (x : m α) :
                                                                                  m α
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    Equations
                                                                                    • Lean.Elab.getInfoTrees = do let __do_liftLean.Elab.getInfoState pure __do_lift.trees
                                                                                    Instances For