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 : PropertyType
• Enumeration : PropertyType
• Binary : PropertyType
• String : PropertyType
• Numeric : PropertyType
• Miscellaneous : PropertyType

inductive Unicode.PropertyName : Type

Property names, extends Basic Unicode Support Level 1 properties

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

def Unicode.instBEqPropertyName.beq : PropertyName → PropertyName → Bool

Equations

• Unicode.instBEqPropertyName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Unicode.instBEqPropertyName : BEq PropertyName

Equations

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

instance Unicode.instToStringPropertyName : ToString PropertyName

Equations

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

def Unicode.typeOfProperty : PropertyName → PropertyType

get type of property

Equations

• Unicode.typeOfProperty Unicode.PropertyName.General_Category = Unicode.PropertyType.Enumeration
• Unicode.typeOfProperty Unicode.PropertyName.Script = Unicode.PropertyType.Enumeration
• Unicode.typeOfProperty Unicode.PropertyName.Alphabetic = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Uppercase = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Lowercase = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.White_Space = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Noncharacter_Code_Point = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Default_Ignorable_Code_Point = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.ANY = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.ASCII = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.ASSIGNED = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Numeric_Value = Unicode.PropertyType.Numeric
• Unicode.typeOfProperty Unicode.PropertyName.Hex_Digit = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.ASCII_Hex_Digit = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Emoji = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Extended_Pictographic = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Grapheme_Cluster_Break = Unicode.PropertyType.Enumeration
• Unicode.typeOfProperty Unicode.PropertyName.Sentence_Break = Unicode.PropertyType.Enumeration
• Unicode.typeOfProperty Unicode.PropertyName.Word_Break = Unicode.PropertyType.Enumeration
• Unicode.typeOfProperty Unicode.PropertyName.Math = Unicode.PropertyType.Binary
• Unicode.typeOfProperty Unicode.PropertyName.Regional_Indicator = Unicode.PropertyType.Binary

structure Unicode.PropertyAlias : Type

Property name palias

• short : String
• long : String
• propertyName : PropertyName

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

Equations

• Unicode.matchPropertyAlias s palias = (decide (Unicode.normalize s = palias.short) || decide (Unicode.normalize s = Unicode.normalize palias.long))

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

get PropertyValueAlias of property name and value

Equations

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

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

get PropertyName of property name s

Equations

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

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

get GeneralCategory of long property value s

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

get GeneralCategory of property value s

Equations

• Unicode.GeneralCategory.ofValue? s = (Unicode.GC.ofAbbrev? s <|> Unicode.GeneralCategory.ofLong? s)

def Unicode.ofValue? (s : String) : Option 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 (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.