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

    Base structure for TermInfo, CommandInfo and TacticInfo.

    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
                    • widgetId : Lake.Name

                      Id of WidgetSource object to use.

                    • props : Lean.Json

                      Json representing the props to be loaded in to the component.

                    An info that represents a user-widget. User-widgets are custom pieces of code that run on the editor client. You can learn about user widgets at src/Lean/Widget/UserWidget

                    Instances For
                      Equations

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