Documentation

Lean.Elab.InfoTree.Types

Context after executing liftTermElabM. Note that the term information collected during elaboration may contain metavariables, and their assignments are stored at mctx.

Instances For

    Context from the root of the InfoTree up to this node. Note that the term information collected during elaboration may contain metavariables, and their assignments are stored at mctx.

    Instances For

      Context for a sub-InfoTree.

      Within InfoTree, this must fulfill the invariant that every non-commandCtx PartialContextInfo node is always contained within a commandCtx node.

      Instances For

        Base structure for TermInfo, CommandInfo and TacticInfo.

        • elaborator : Lake.Name

          The name of the elaborator that created this info.

        • The piece of syntax that the elaborator created this info for. Note that this also implicitly stores the code position in the syntax's SourceInfo.

        Instances For
          Equations
          Instances For
            Equations
              Instances For

                Info for an option reference (e.g. in set_option).

                Instances For
                  Instances For
                    Equations

                    The information needed to render the tactic state in the infoview.

                    We store the list of goals before and after the execution of a tactic. We also store the metavariable context at each time since we want metavariables unassigned at tactic execution time to be displayed as ?m....

                    Instances For
                      Equations
                      Equations

                      Dynamic info for custom use cases.

                      Instances For

                        Information about a user widget associated with a syntactic span. This must be a panel widget. A panel widget is a widget that can be displayed in the infoview alongside the goal state.

                        Instances For

                          Specifies that the given free variables should be considered semantically identical. The free variable baseId might not be in the current local context because it has been cleared. Used for e.g. connecting variables before and after match generalization.

                          Instances For

                            Contains the syntax of an identifier which is part of a field redeclaration, like:

                            structure Foo := x : Nat
                            structure Bar extends Foo :=
                              x := 0
                            --^ here
                            
                            Instances For

                              Denotes information for the term that is emitted by the delaborator when omitting a term due to pp.deepTerms false or pp.proofs false. Omission needs to be treated differently from regular terms because it has to be delaborated differently in Lean.Widget.InteractiveDiagnostics.infoToInteractive: Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with regular delaboration settings.

                              Instances For
                                inductive Lean.Elab.Info :

                                Header information for a node in InfoTree.

                                Instances For

                                  The InfoTree is a structure that is generated during elaboration and used by the language server to look up information about objects at particular points in the Lean document. For example, tactic information and expected type information in the infoview and information about completions.

                                  The infotree consists of nodes which may have child nodes. Each node has an Info object that contains details about what kind of information is present. Each Info object also contains a Syntax instance, this is used to map positions in the Lean document to particular info objects.

                                  An example of a function that extracts information from an infotree for a given position is InfoTree.goalsAt? which finds TacticInfo.

                                  Information concerning expressions requires that a context also be saved. context nodes store a local context that is used to process expressions in nodes below.

                                  Because the info tree is generated during elaboration, some parts of the infotree for a particular piece of syntax may not be ready yet. Hence InfoTree supports metavariable-like holes which are filled in later in the same way that unassigned metavariables are.

                                  Instances For

                                    This structure is the state that is being used to build an InfoTree object. During elaboration, some parts of the info tree may be holes which need to be filled later. The assignments field is used to assign these holes. The trees field is a list of pending child trees for the infotree node currently being built.

                                    You should not need to use InfoState directly, instead infotrees should be built with the help of the methods here such as pushInfoLeaf to create leaf nodes and withInfoContext to create a nested child node.

                                    To see how trees is used, look at the function body of withInfoContext'.

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