GraphemeBreakProperty

Properties of file GraphemeBreakProperty

structure Unicode.GraphemeBreakProperty : Type

• name : String
• properties : Array (UInt32 × Option UInt32)

instance Unicode.instToStringGraphemeBreakProperty : ToString GraphemeBreakProperty

Equations

• Unicode.instToStringGraphemeBreakProperty = { toString := fun (s : Unicode.GraphemeBreakProperty) => toString s.name ++ toString " " ++ toString s.properties }

def Unicode.GraphemeBreakProperty.txt : String

Equations

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

def Unicode.GraphemeBreakProperty.data : Array GraphemeBreakProperty

Equations

• Unicode.GraphemeBreakProperty.data = #[]

def Unicode.rangesOfGraphemeBreak (s : String) : Except String (Array (NonemptyInterval Char))

Equations

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