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

• 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 : Unicode.PropertyName

def Unicode.matchPropertyAlias (s : String) (palias : Unicode.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 : 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

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

get GeneralCategory of long property value s

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

get GeneralCategory of property value s

Equations

• Unicode.GeneralCategory.ofValue? s = (Unicode.GeneralCategory.ofAbbrev? s <|> 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.