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

fix(tests/playground/parser/parser): small bugs

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-12 08:58:02 -07:00
parent 48ba69775a
commit d7de85e1e7
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/playground/parser/parser.lean
View file

@ -368,7 +368,7 @@ def numberFnAux : ParserFn
else if c == 'x' || c == 'X' then
hexNumberFn startPos s (d.next s i)
else
decimalNumberFn startPos s (d.next s i)
decimalNumberFn startPos s (d.setPos i)
else if c.isDigit then
decimalNumberFn startPos s (d.next s startPos)
else
@ -407,6 +407,7 @@ match tk with
let val := tk.val in
let stopPos := startPos + val.bsize in
let d := d.setPos stopPos in
let d := whitespace s d in
let wsStopPos := d.pos in
let trailing := { Substring . str := s, startPos := stopPos, stopPos := wsStopPos } in
let atom := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val in