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

fix: ignore empty character literals

Browse source
This commit is contained in:
Sebastian Ullrich 2022-12-08 13:51:11 +01:00 • committed by Gabriel Ebner
parent f3f4eba945
commit 9c9cc017df
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Basic.lean
View file

@ -786,7 +786,7 @@ private def tokenFnAux : ParserFn := fun c s =>
let curr := input.get i
if curr == '\"' then
strLitFnAux i c (s.next input i)
else if curr == '\'' then
else if curr == '\'' && getNext input i != '\'' then
charLitFnAux i c (s.next input i)
else if curr.isDigit then
numberFnAux c s