From c4121e779d0630c59667c448d75ae416fb339847 Mon Sep 17 00:00:00 2001 From: Chris Lovett Date: Fri, 5 Aug 2022 13:06:21 -0700 Subject: [PATCH] =?UTF-8?q?fix:=20hexDigit=20('a'=20=E2=89=A4=20c=20?= =?UTF-8?q?=E2=88=A7=20c=20=E2=89=A4=20'f')?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Lean/Data/Parsec.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Data/Parsec.lean b/src/Lean/Data/Parsec.lean index c702dab95c..5e4c889a94 100644 --- a/src/Lean/Data/Parsec.lean +++ b/src/Lean/Data/Parsec.lean @@ -124,8 +124,8 @@ def digit : Parsec Char := attempt do def hexDigit : Parsec Char := attempt do let c ← anyChar if ('0' ≤ c ∧ c ≤ '9') - ∨ ('a' ≤ c ∧ c ≤ 'a') - ∨ ('A' ≤ c ∧ c ≤ 'A') then return c else fail s!"hex digit expected" + ∨ ('a' ≤ c ∧ c ≤ 'f') + ∨ ('A' ≤ c ∧ c ≤ 'F') then return c else fail s!"hex digit expected" @[inline] def asciiLetter : Parsec Char := attempt do