Documentation

Lean.Data.Position

structure Lean.Position :
Instances For
    Equations
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      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.

      • lines : Array Nat

        The line numbers associated with the positions. Has the same length as positions and is always of the form #[1, 2, …, n-1, n-1].

      Instances For
        Equations
        class Lean.MonadFileMap (m : TypeType) :
        Instances
          partial def Lean.FileMap.ofString.loop (s : String) (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            partial def Lean.FileMap.toPosition.loop (pos : String.Pos) (str : String) (ps : Array String.Pos) (lines : Array Nat) (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 stame result as map.ofPosition ⟨line, 0⟩, but is more efficient.

              Equations
              Instances For