From 9c9cc017df27e4bb185287a671cfbb479fd01a7a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 8 Dec 2022 13:51:11 +0100 Subject: [PATCH] fix: ignore empty character literals --- src/Lean/Parser/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 5dc1c956ed..0eb426b3ad 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -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