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
• = if c.val 65535 then 1 else 2
Equations

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

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

Equations

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

Equations

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.
Equations
• One or more equations did not get rendered due to their size.