INNER CODE UNIT · Python
identifierStartFlag
lean-dojo/TorchLean · scripts/generate_unicode_table.py:192
def identifierStartFlag : UInt8 := {IDENTIFIER_START}
/-- Flag bit recording that the character may continue an identifier. -/
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