Skip to content

Commit

Permalink
add doc comments
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Jan 26, 2024
1 parent a524fd4 commit 0bc66dc
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions src/Lean/Data/Position.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 indices. Has the same length as `positions` and is always of the form
`[1, 2, …, n-1, n-1]`. -/
lines : Array Nat
deriving Inhabited

Expand Down

0 comments on commit 0bc66dc

Please sign in to comment.