Documentation

Lean.Data.Lsp.Utf16

LSP uses UTF-16 for indexing, so we need to provide some primitives to interact with Lean strings using UTF-16 indices.

Equations
Instances For
    Equations
    Instances For

      Computes the UTF-16 offset of the n-th Unicode codepoint in the substring of s starting at UTF-8 offset off. Yes, this is actually useful.

      Equations
      Instances For

        Computes the position of the Unicode codepoint at UTF-16 offset utf16pos in the substring of s starting at UTF-8 offset off.

        Equations
        Instances For

          Starting at utf8pos, finds the UTF-8 offset of the p-th codepoint.

          Equations
          Instances For

            Computes an UTF-8 offset into text.source from an LSP-style 0-indexed (ln, col) position.

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