Documentation

Lean.Syntax

structure String.Range :

A position range inside a string. This type is mostly in combination with syntax trees, as there might not be a single underlying string in this case that could be used for a Substring.

Instances For
    def String.Range.contains (r : String.Range) (pos : Pos) (includeStop : Bool := false) :
    Equations
      Instances For
        def String.Range.includes (super sub : String.Range) (includeSuperStop includeSubStop : Bool := false) :

        Checks whether sub is contained in super. includeSuperStop and includeSubStop control whether super and sub have an inclusive upper bound.

        Equations
          Instances For
            def String.Range.overlaps (first second : String.Range) (includeFirstStop includeSecondStop : Bool := false) :
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For

                                Converts an original or synthetic (canonical := true) SourceInfo to a synthetic (canonical := false) SourceInfo. This is sometimes useful when SourceInfo is being moved around between Syntaxes.

                                Equations
                                  Instances For

                                    Syntax AST #

                                    inductive Lean.IsNode :
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              def Lean.unreachIsNodeAtom {β : Sort u_1} {info : SourceInfo} {val : String} :
                                              IsNode (Syntax.atom info val)β
                                              Equations
                                                Instances For
                                                  def Lean.unreachIsNodeIdent {β : Sort u_1} {info : SourceInfo} {rawVal : Substring} {val : Name} {preresolved : List Syntax.Preresolved} :
                                                  IsNode (Syntax.ident info rawVal val preresolved)β
                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          @[inline]
                                                          Equations
                                                            Instances For
                                                              @[inline]
                                                              def Lean.SyntaxNode.withArgs {β : Sort u_1} (n : SyntaxNode) (fn : Array Syntaxβ) :
                                                              β
                                                              Equations
                                                                Instances For
                                                                  @[inline]
                                                                  Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              Equations
                                                                                Instances For

                                                                                  Compares syntax structures and position ranges, but not whitespace. We generally assume that if syntax trees equal in this way generate the same elaboration output, including positions contained in e.g. diagnostics and the info tree. However, as we have a few request handlers such as goalsAt? that are sensitive to whitespace information in the info tree, we currently use eqWithInfo instead for reuse checks.

                                                                                  Like structRangeEq but prints trace on failure if trace.Elab.reuse is activated.

                                                                                  Equations
                                                                                    Instances For

                                                                                      Full comparison of syntax structures and source infos.

                                                                                      Like eqWithInfo but prints trace on failure if trace.Elab.reuse is activated.

                                                                                      Equations
                                                                                        Instances For
                                                                                          Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  def Lean.Syntax.ifNode {β : Sort u_1} (stx : Syntax) (hyes : SyntaxNodeβ) (hno : Unitβ) :
                                                                                                  β
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      def Lean.Syntax.ifNodeKind {β : Sort u_1} (stx : Syntax) (kind : SyntaxNodeKind) (hyes : SyntaxNodeβ) (hno : Unitβ) :
                                                                                                      β
                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              def Lean.Syntax.getIdAt (stx : Syntax) (i : Nat) :
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  partial def Lean.Syntax.hasIdent (id : Name) :

                                                                                                                  Check for a Syntax.ident of the given name anywhere in the tree. This is usually a bad idea since it does not check for shadowing bindings, but in the delaborator we assume that bindings are never shadowed.

                                                                                                                  @[inline]
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      def Lean.Syntax.modifyArg (stx : Syntax) (i : Nat) (fn : SyntaxSyntax) :
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          @[specialize #[]]
                                                                                                                          partial def Lean.Syntax.replaceM {m : TypeType} [Monad m] (fn : Syntaxm (Option Syntax)) :
                                                                                                                          @[specialize #[]]
                                                                                                                          partial def Lean.Syntax.rewriteBottomUpM {m : TypeType} [Monad m] (fn : Syntaxm Syntax) :
                                                                                                                          @[inline]
                                                                                                                          Equations
                                                                                                                            Instances For

                                                                                                                              Set SourceInfo.leading according to the trailing stop of the preceding token. The result is a round-tripping syntax tree IF, in the input syntax tree,

                                                                                                                              • all leading stops, atom contents, and trailing starts are correct
                                                                                                                              • trailing stops are between the trailing start and the next leading stop.

                                                                                                                              Remark: after parsing, all SourceInfo.leading fields are empty. The Syntax argument is the output produced by the parser for source. This function "fixes" the source.leading field.

                                                                                                                              Additionally, we try to choose "nicer" splits between leading and trailing stops according to some heuristics so that e.g. comments are associated to the (intuitively) correct token.

                                                                                                                              Note that the SourceInfo.trailing fields must be correct. The implementation of this Function relies on this property.

                                                                                                                              Equations
                                                                                                                                Instances For

                                                                                                                                  Split an ident into its dot-separated components while preserving source info. Macro scopes are first erased. For example, `foo.bla.boo._@._hyg.4[`foo, `bla, `boo]. If nFields is set, we take that many fields from the end and keep the remaining components as one name. For example, `foo.bla.boo with (nFields := 1)[`foo.bla, `boo].

                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          Instances For
                                                                                                                                            def Lean.Syntax.topDown (stx : Syntax) (firstChoiceOnly : Bool := false) :

                                                                                                                                            for _ in stx.topDown iterates through each node and leaf in stx top-down, left-to-right. If firstChoiceOnly is true, only visit the first argument of each choice node.

                                                                                                                                            Equations
                                                                                                                                              Instances For
                                                                                                                                                Equations
                                                                                                                                                  @[specialize #[]]
                                                                                                                                                  partial def Lean.Syntax.instForInTopDown.loop {m : Type u_1 → Type u_2} {β✝ : Type u_1} [Monad m] (f : Syntaxβ✝m (ForInStep β✝)) (firstChoiceOnly : Bool) (stx : Syntax) (b : β✝) [Inhabited β✝] :
                                                                                                                                                  m (ForInStep β✝)
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          def Lean.Syntax.getRange? (stx : Syntax) (canonicalOnly : Bool := false) :
                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  def Lean.Syntax.ofRange (range : String.Range) (canonical : Bool := true) :

                                                                                                                                                                  Returns a synthetic Syntax which has the specified String.Range.

                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For

                                                                                                                                                                      Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right. Indices are allowed to be out-of-bound, in which case cur is Syntax.missing. If the Traverser is used linearly, updates are linear in the Syntax object as well.

                                                                                                                                                                      Instances For
                                                                                                                                                                        Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            Equations
                                                                                                                                                                              Instances For

                                                                                                                                                                                Advance to the idx-th child of the current node.

                                                                                                                                                                                Equations
                                                                                                                                                                                  Instances For

                                                                                                                                                                                    Advance to the parent of the current node, if any.

                                                                                                                                                                                    Equations
                                                                                                                                                                                      Instances For

                                                                                                                                                                                        Advance to the left sibling of the current node, if any.

                                                                                                                                                                                        Equations
                                                                                                                                                                                          Instances For

                                                                                                                                                                                            Advance to the right sibling of the current node, if any.

                                                                                                                                                                                            Equations
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                Monad class that gives read/write access to a Traverser.

                                                                                                                                                                                                Instances
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          def Lean.Syntax.mkAntiquotNode (kind : Name) (term : Syntax) (nesting : Nat := 0) (name : Option String := none) (isPseudoKind : Bool := false) :
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                          Return kind of parser expected at this antiquotation, and whether it is a "pseudo" kind (see mkAntiquot).

                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          def Lean.Syntax.mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suffix : String) (nesting : Nat := 0) :
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                              @[reducible, inline]

                                                                                                                                                                                                                                                                                                              List of Syntax nodes in which each succeeding element is the parent of the current. The associated index is the index of the preceding element in the list of children of the current element.

                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                  def Lean.Syntax.findStack? (root : Syntax) (visit : SyntaxBool) (accept : SyntaxBool := fun (stx : Syntax) => !stx.hasArgs) :

                                                                                                                                                                                                                                                                                                                  Return stack of syntax nodes satisfying visit, starting with such a node that also fulfills accept (default "is leaf"), and ending with the root.

                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                      partial def Lean.Syntax.findStack?.go (visit : SyntaxBool) (accept : SyntaxBool := fun (stx : Syntax) => !stx.hasArgs) (stack : Syntax.Stack) (stx : Syntax) :

                                                                                                                                                                                                                                                                                                                      Compare the SyntaxNodeKinds in pattern to those of the Syntax elements in stack. Return false if stack is shorter than pattern.

                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                        Instances For