Documentation

Lean.Data.Position

structure Lean.Position :
Instances For
    Equations
    Equations
    • x✝.lt x = match x✝, x with | { line := l₁, column := c₁ }, { line := l₂, column := c₂ } => decide ((l₁, c₁).lexLt (l₂, c₂))
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      structure Lean.FileMap :

      Content of a file together with precalculated positions of newlines.

      • source : String

        The content of the file.

      • positions : Array String.Pos

        The positions of newline characters. The first entry is always 0 and the last always the index of the last character. In particular, if the last character is a newline, that index will appear twice.

      Instances For
        Equations
        class Lean.MonadFileMap (m : TypeType) :
        Instances

          The last line should always be positions.size - 1.

          Equations
          • fmap.getLastLine = fmap.positions.size - 1
          Instances For

            The line numbers associated with the positions of the FileMap. fmap.getLine i is the iᵗʰ entry of #[1, 2, …, n-1, n-1] where n is the size of positions.

            Equations
            • fmap.getLine x = min (x + 1) fmap.getLastLine
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                partial def Lean.FileMap.toPosition.loop (fmap : Lean.FileMap) (pos : String.Pos) (str : String) (ps : Array String.Pos) (b : Nat) (e : Nat) :

                Convert a Lean.Position to a String.Pos.

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

                  Returns the position of the start of (1-based) line line. This gives the same result as map.ofPosition ⟨line, 0⟩, but is more efficient.

                  Equations
                  • map.lineStart line = if h : line - 1 < map.positions.size then map.positions.get line - 1, h else map.positions.back?.getD 0
                  Instances For
                    Equations
                    Instances For