@[reducible, inline]

abbrev Unicode.Scripts : Type

Type for scripts data

Equations

• Unicode.Scripts = Std.HashMap String.Slice (Array (UInt32 × UInt32))

def Unicode.Scripts.txt : String

Raw string from Scripts.txt

Equations

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

opaque Unicode.Scripts.data : Scripts

@[inline]

def Unicode.Scripts.getTable? (sc : String.Slice) : Option (Array (UInt32 × UInt32))

Get table for given script

Equations

• Unicode.Scripts.getTable? sc = do let sc ← some (Unicode.PropertyValueAliases.getLongName! "Script".toSlice sc) Std.HashMap.get? Unicode.Scripts.data sc

@[inline]

def Unicode.Scripts.getTable! (sc : String.Slice) : Array (UInt32 × UInt32)

Get table for given script

Equations

• Unicode.Scripts.getTable! sc = (Unicode.Scripts.getTable? sc).get!