Unicode

Support for Unicode Regular Expressions Level 1

def Unicode.rangesOfGeneralCategory (category : GeneralCategory) : Except String (Array (NonemptyInterval Char))

Equations

• One or more equations did not get rendered due to their size.

def Unicode.rangesOfNamedProperty (name prop : String) : Except String (Array (NonemptyInterval Char))

Equations

• One or more equations did not get rendered due to their size.

def Unicode.rangesOfProperty (prop : String) : Except String (Array (NonemptyInterval Char))

Equations

• One or more equations did not get rendered due to their size.

def Unicode.is_word_char (c : Char) : Bool

has c the word property

Equations

• Unicode.is_word_char c = Unicode.isCharInIntervals✝ c (Unicode.rangesOfProperty "Word")

def Unicode.isCharOfGeneralCategory (category : GeneralCategory) (c : Char) : Bool

has c the general category

Equations

• Unicode.isCharOfGeneralCategory category c = Unicode.isCharInIntervals✝ c (Unicode.rangesOfGeneralCategory category)

def Unicode.case_fold_char (c : Char) : Array (NonemptyInterval Char)

get ranges of case folds of char

Equations

• One or more equations did not get rendered due to their size.

theorem Unicode.Fin.sub_le_of_le {n : Nat} {a b : Fin n} (h : a ≤ b) : b - a ≤ b

theorem Unicode.Uint32.sub_le_of_le {a b : UInt32} (h : a ≤ b) : b - a ≤ b

def Unicode.case_fold_range (r : NonemptyInterval Char) : Array (NonemptyInterval Char)

get ranges of case folds of chars in range

Equations

• Unicode.case_fold_range r = Array.flatMap (fun (c : Char) => Unicode.case_fold_char c) (Unicode.loop✝ r.fst 0 ↑(r.snd.val - r.fst.val).toFin #[] Unicode.case_fold_range._proof_18 ⋯)