Documentation

Std.Lean.Position

Return the beginning of the line contatining character pos.

Equations

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