Unicode character properties

A unicode character may have properties. A property has a name and a type (Unicode.PropertyType) and may have values.

see

• Basic Unicode Support Level 1 properties
• Extended Unicode Support Level 2 full properties

inductive Unicode.PropertyType : Type

The type of a property

• Catalog: Unicode.PropertyType
• Enumeration: Unicode.PropertyType
• Binary: Unicode.PropertyType
• String: Unicode.PropertyType
• Numeric: Unicode.PropertyType
• Miscellaneous: Unicode.PropertyType

inductive Unicode.PropertyName : Type

Property names, extends Basic Unicode Support Level 1 properties

• General_Category: Unicode.PropertyName
• Script: Unicode.PropertyName
• Alphabetic: Unicode.PropertyName
• Uppercase: Unicode.PropertyName
• Lowercase: Unicode.PropertyName
• White_Space: Unicode.PropertyName
• Noncharacter_Code_Point: Unicode.PropertyName
• Default_Ignorable_Code_Point: Unicode.PropertyName
• ANY: Unicode.PropertyName
• ASCII: Unicode.PropertyName
• ASSIGNED: Unicode.PropertyName
• Numeric_Value: Unicode.PropertyName
• Hex_Digit: Unicode.PropertyName
• ASCII_Hex_Digit: Unicode.PropertyName
• Emoji: Unicode.PropertyName
• Extended_Pictographic: Unicode.PropertyName
• Grapheme_Cluster_Break: Unicode.PropertyName
• Sentence_Break: Unicode.PropertyName
• Word_Break: Unicode.PropertyName
• Math: Unicode.PropertyName
• Regional_Indicator: Unicode.PropertyName

instance Unicode.instBEqPropertyName : BEq Unicode.PropertyName

Equations

• Unicode.instBEqPropertyName = { beq := Unicode.beqPropertyName✝ }

instance Unicode.instToStringPropertyName : ToString Unicode.PropertyName

Equations

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

def Unicode.typeOfProperty : Unicode.PropertyName → Unicode.PropertyType

get type of property

Equations

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

structure Unicode.PropertyAlias : Type

Property name palias

• short : String
• long : String
• propertyName : Unicode.PropertyName

def Unicode.matchPropertyAlias (s : String) (palias : Unicode.PropertyAlias) : Bool

Equations

• Unicode.matchPropertyAlias s palias = let sn := Unicode.normalize s; let ln := Unicode.normalize palias.long; decide (sn = palias.short) || decide (sn = ln)

def Unicode.getPropertyValueAlias (name : Unicode.PropertyName) (val : String) : Option Unicode.PropertyAlias

get PropertyValueAlias of property name and value

Equations

• Unicode.getPropertyValueAlias name val = match Unicode.propertyValueAliases.find? (Unicode.matchPropertyValueAlias name val) with | some palias => some palias | none => none

def Unicode.ofName? (s : String) : Option Unicode.PropertyName

get PropertyName of property name s

Equations

• Unicode.ofName? s = match Unicode.propertyAliases.find? (Unicode.matchPropertyAlias s) with | some palias => some palias.propertyName | none => none

def Unicode.GeneralCategory.ofLong? (s : Substring) : Option Unicode.GeneralCategory

get GeneralCategory of long property value s

Equations

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

def Unicode.GeneralCategory.ofValue? (s : Substring) : Option Unicode.GeneralCategory

get GeneralCategory of property value s

Equations

• Unicode.GeneralCategory.ofValue? s = HOrElse.hOrElse (Unicode.GeneralCategory.ofAbbrev? s) fun (x : Unit) => Unicode.GeneralCategory.ofLong? s

def Unicode.ofValue? (s : String) : Option Unicode.PropertyName

get PropertyName of property value

Equations

• Unicode.ofValue? s = match Unicode.GeneralCategory.ofValue? s.toSubstring with | some val => some Unicode.PropertyName.General_Category | none => none

def Unicode.ofCompatibilityPropertyName? (s : String) : Option (Array (Unicode.PropertyName × Option String))

get PropertyName of compatibility property name, see Compatibility_Properties

Equations

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