perf: inline IsUTF8FirstByte

2026-04-01 01:34:06 +00:00 · 2026-01-02 10:58:08 +00:00
1 changed files with 1 additions and 0 deletions
--- a/src/Init/Data/String/Decode.lean
+++ b/src/Init/Data/String/Decode.lean
@@ -1396,6 +1396,7 @@ scalar value.
 public def IsUTF8FirstByte (c : UInt8) : Prop :=
  c &&& 0x80 = 0 ∨ c &&& 0xe0 = 0xc0 ∨ c &&& 0xf0 = 0xe0 ∨ c &&& 0xf8 = 0xf0

+@[inline]
 public instance {c : UInt8} : Decidable c.IsUTF8FirstByte :=
  inferInstanceAs <| Decidable (c &&& 0x80 = 0 ∨ c &&& 0xe0 = 0xc0 ∨ c &&& 0xf0 = 0xe0 ∨ c &&& 0xf8 = 0xf0)