Script

Properties of file Scripts.

structure Unicode.Script : Type

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

instance Unicode.instToStringScript : ToString Unicode.Script

Equations

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

def Unicode.ScriptProperties.txt : String

Equations

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

def Unicode.ScriptProperties.data : Array Unicode.Script

Equations

• Unicode.ScriptProperties.data = #[]

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

Equations

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

def Unicode.Script.names : Array String

Equations

• Unicode.Script.names = Array.map (fun (x : Unicode.Script) => x.name) Unicode.ScriptProperties.data