INNER CODE UNIT · Python
identifierContinueFlag
lean-dojo/TorchLean · scripts/generate_unicode_table.py:195
def identifierContinueFlag : UInt8 := {IDENTIFIER_CONTINUE}
/-- Flag bit recording `str.isdecimal`. -/
def decimalFlag : UInt8 := {DECIMAL}
{table}
/--
The property run containing a character, if it has any recorded property.
The structural fuel keeps lookup reducible in kernel proofs of the lexer. The pinned
`Array.binSearch` implementation does not reduce through the imported module boundary.
-/
def lookup? (char : Char) : Option Interval :=
search char.val intervals.size 0 intervals.size
where
search (codepoint : UInt32) : (fuel lo hi : Nat) → Option Interval
| 0, _, _ => none
| fuel + 1, lo, hi =>