@[instance_reducible]

instance Lean.instOrdRange_importGraph : Ord Syntax.Range

Equations

• Lean.instOrdRange_importGraph = { compare := Lean.instOrdRange_importGraph.ord }

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

Equations

• Lean.instOrdRange_importGraph.ord { start := a, stop := a_1 } { start := b, stop := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

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.

Equations

• stx.updateLeadingPreservingStart = StateT.run' (Lean.Syntax.replaceM Lean.Syntax.updateLeadingAux✝ stx) (stx.getPos?.getD 0)

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.

Equations

• stx.updateLeadingPreservingStart = { raw := stx.raw.updateLeadingPreservingStart }

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

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

Equations

• (Lean.SourceInfo.original leading pos trailing endPos).getLeading? = some leading
• x✝.getLeading? = none

@[inline]

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

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

Equations

• info.getLeading = info.getLeading?.getD "".toRawSubstring

@[inline]

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

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

Equations

• info.getTrailing = info.getTrailing?.getD "".toRawSubstring

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.

Equations

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

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.

Equations

• (Lean.SourceInfo.original leading pos trailing endPos).getOriginalLeadingPos? = some leading.startPos
• x✝.getOriginalLeadingPos? = none

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.

Equations

• (Lean.SourceInfo.original leading pos trailing endPos).getLeadingPos? canonicalOnly = some leading.startPos
• (Lean.SourceInfo.synthetic pos endPos true).getLeadingPos? canonicalOnly = some pos
• (Lean.SourceInfo.synthetic pos endPos canonical).getLeadingPos? = some pos
• info.getLeadingPos? canonicalOnly = none

@[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.

Equations

• stx.getLeadingPos? canonicalOnly = stx.getHeadInfo.getLeadingPos? canonicalOnly