max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add doc for FileMap (#3221)

Browse source
This commit is contained in:
Jon Eugster 2024-01-31 22:51:37 +01:00 • committed by GitHub
parent c98deeb709
commit 1cb1602977
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Data/Position.lean
View file

@ -29,9 +29,16 @@ instance : ToExpr Position where
end Position
/-- Content of a file together with precalculated positions of newlines. -/
structure FileMap where
/-- The content of the file. -/
source : String
/-- 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. -/
positions : Array String.Pos
/-- 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]`. -/
lines : Array Nat
deriving Inhabited