Documentation

Batteries.Lean.Position

source
@[deprecated Lean.FileMap.lspRangeOfStx? (since := "2025-09-23")]
def Lean.FileMap.rangeOfStx? (text : FileMap) (stx : Syntax) :
Option Lsp.Range

Gets the LSP range of syntax stx.

Instances For
    source
    def Lean.findLineStart (s : String) (pos : String.Pos.Raw) :
    String.Pos.Raw

    Return the beginning of the line contatining character pos.

    Instances For
      source
      def Lean.findIndentAndIsStart (s : String) (pos : String.Pos.Raw) :
      Nat × Bool

      Return the indentation (number of leading spaces) of the line containing pos, and whether pos is the first non-whitespace character in the line.

      Instances For