Documentation

Std.Lean.Position

Gets the LSP range from a String.Range.

Equations
Instances For

    Gets the LSP range of syntax stx.

    Equations
    Instances For

      Convert a Lean.Position to a String.Pos.

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

        Return the beginning of the line contatining character pos.

        Equations
        Instances For

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

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

            Returns a synthetic Syntax which has the specified String.Range.

            Equations
            Instances For

              Returns the position of the start of (1-based) line line.

              Equations
              Instances For