- MkPosition : (line : Nat) ->
(offset : Nat) ->
Position
- line
Line number (starting from 0)
- offset
Character offset in the given line
- record Position
Position in the input string
- MkPosition : (line : Nat) ->
(offset : Nat) ->
Position
- line
Line number (starting from 0)
- offset
Character offset in the given line
- line : (rec : Position) ->
Nat
Line number (starting from 0)
- offset : (rec : Position) ->
Nat
Character offset in the given line
- next : Char ->
Position ->
Position
- start : Position
- update : Char ->
Position ->
Position
Every Char induces an action on Positions
- updates : String ->
Position ->
Position