@[instance_reducible]

instance Lean.instOrdRange_importGraph : Ord Syntax.Range

def Lean.instOrdRange_importGraph.ord : Syntax.Range → Syntax.Range → Ordering

def Lean.Syntax.updateLeadingPreservingStart : Syntax → Syntax

Like Lean.Syntax.updateLeading, but preserves the starting position of the syntax if it exists (instead of setting it to 0). See the docstring of updateLeading for more details.

def Lean.TSyntax.updateLeadingPreservingStart {ks : SyntaxNodeKinds} (stx : TSyntax ks) : TSyntax ks

Like Lean.TSyntax.updateLeading, but preserves the starting position of the syntax if it exists (instead of setting it to 0). See the docstring of updateLeading for more details.

def Lean.SourceInfo.getLeading? : SourceInfo → Option Substring.Raw

Gets the leading whitespace of .original SourceInfo, or none if not .original.

@[inline]

def Lean.SourceInfo.getLeading (info : SourceInfo) : Substring.Raw

Gets the leading whitespace of .original SourceInfo, or the empty substring if not .original.

@[inline]

def Lean.SourceInfo.getTrailing (info : SourceInfo) : Substring.Raw

Gets the trailing whitespace of .original SourceInfo, or the empty substring if not .original.

def Lean.Syntax.unsetLeading (stx : Syntax) : Syntax

Clear the leading whitespace of the given syntax if the head SourceInfo is .original, and otherwise leave it unchanged. See Syntax.unsetTrailing for removing trailing whitespace.

def Lean.SourceInfo.getOriginalLeadingPos? : SourceInfo → Option String.Pos.Raw

Get the start position of the leading whitespace of .original SourceInfo, or none if it is not .original.

def Lean.SourceInfo.getLeadingPos? (info : SourceInfo) (canonicalOnly : Bool := false) : Option String.Pos.Raw

Get the start position of the leading whitespace of .original SourceInfo, or the start position of .synthetic SourceInfo (and none otherwise).

If canonicalOnly := false (the default), also returns none on non-canonical .synthetic SourceInfo.

@[inline]

def Lean.Syntax.getLeadingPos? (stx : Syntax) (canonicalOnly : Bool := false) : Option String.Pos.Raw

Get the start position of the leading whitespace of the Syntax if it is original, or the start position if synthetic (and none otherwise).

If canonicalOnly := false (the default), also returns none on non-canonical synthetic Syntax.