Unicode.Includes

source

partial def String.splitOn'Aux (s : String) (sep : String) (b : String.Pos) (i : String.Pos) (j : String.Pos) (r : Array String) :

Array String

source

def String.splitOn' (s : String) (sep : optParam String " ") :

Array String

Equations

String.splitOn' s sep = if (sep == "") = true then #[s] else String.splitOn'Aux s sep 0 0 0 #[]

Included Raw Strings #

UCD Main Directory #

source

def Unicode.arabicShapingStr:

String

Includes the ArabicShaping.txt string.

Equations

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

source

def Unicode.bidiBracketsStr:

String

Includes the BidiBrackets.txt string.

Equations

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

source

def Unicode.bidiMirroringStr:

String

Includes the BidiMirroring.txt string.

Equations

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

source

def Unicode.normalizationCorrectionsStr:

String

Includes the NormalizationCorrections.txt string.

Equations

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

source

def Unicode.blocksStr:

String

Includes the Blocks.txt string.

Equations

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

source

def Unicode.nushuSourcesStr:

String

Includes the NushuSources.txt string.

Equations

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

source

def Unicode.propListStr:

String

Includes the PropList.txt string.

Equations

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

source

def Unicode.caseFoldingStr:

String

Includes the CaseFolding.txt string.

Equations

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

source

def Unicode.compositionExclusionsStr:

String

Includes the CompositionExclusions.txt string.

Equations

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

source

def Unicode.derivedAgeStr:

String

Includes the DerivedAge.txt string.

Equations

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

source

def Unicode.scriptExtensionsStr:

String

Includes the ScriptExtensions.txt string.

Equations

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

source

def Unicode.derivedCorePropertiesStr:

String

Includes the DerivedCoreProperties.txt string.

Equations

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

source

def Unicode.scriptsStr:

String

Includes the Scripts.txt string.

Equations

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

source

def Unicode.derivedNormalizationPropsStr:

String

Includes the DerivedNormalizationProps.txt string.

Equations

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

source

def Unicode.specialCasingStr:

String

Includes the SpecialCasing.txt string.

Equations

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

source

def Unicode.eastAsianWidthStr:

String

Includes the EastAsianWidth.txt string.

Equations

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

source

def Unicode.equivalentUnifiedIdeographStr:

String

Includes the EquivalentUnifiedIdeograph.txt string.

Equations

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

source

def Unicode.hangulSyllableTypeStr:

String

Includes the HangulSyllableType.txt string.

Equations

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

source

def Unicode.unicodeDataStr:

String

Includes the UnicodeData.txt string. See unicodeDataMap.

Equations

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

source

def Unicode.indicPositionalCategoryStr:

String

Includes the IndicPositionalCategory.txt string.

Equations

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

source

def Unicode.verticalOrientationStr:

String

Includes the VerticalOrientation.txt string.

Equations

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

source

def Unicode.indicSyllabicCategoryStr:

String

Includes the IndicSyllabicCategory.txt string.

Equations

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

source

def Unicode.jamoStr:

String

Includes the Jamo.txt string.

Equations

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

source

def Unicode.lineBreakStr:

String

Includes the LineBreak.txt string.

Equations

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

source

def Unicode.nameAliasesStr:

String

Includes the NameAliases.txt string.

Equations

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

Auxiliary Subdirectory #

source

def Unicode.graphemeBreakPropertyStr:

String

Includes the GraphemeBreakProperty.txt string.

Equations

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

source

def Unicode.wordBreakPropertyStr:

String

Includes the WordBreakProperty.txt string.

Equations

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

source

def Unicode.sentenceBreakPropertyStr:

String

Includes the SentenceBreakProperty.txt string.

Equations

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

Emoji Subdirectory #

source

def Unicode.emojiDataStr:

String

Includes the emoji-data.txt string.

Equations

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

Extracted Subdirectory #

source

def Unicode.derivedBidiClassStr:

String

Includes the DerivedBidiClass.txt string.

Equations

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

source

def Unicode.derivedJoiningGroupStr:

String

Includes the DerivedJoiningGroup.txt string.

Equations

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

source

def Unicode.derivedBinaryPropertiesStr:

String

Includes the DerivedBinaryProperties.txt string.

Equations

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

source

def Unicode.derivedJoiningTypeStr:

String

Includes the DerivedJoiningType.txt string.

Equations

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

source

def Unicode.derivedCombiningClassStr:

String

Includes the DerivedCombiningClass.txt string.

Equations

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

source

def Unicode.derivedLineBreakStr:

String

Includes the DerivedLineBreak.txt string.

Equations

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

source

def Unicode.derivedDecompositionTypeStr:

String

Includes the DerivedDecompositionType.txt string.

Equations

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

source

def Unicode.derivedNameStr:

String

Includes the DerivedName.txt string.

Equations

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

source

def Unicode.derivedEastAsianWidthStr:

String

Includes the DerivedEastAsianWidth.txt string.

Equations

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

source

def Unicode.derivedNumericTypeStr:

String

Includes the DerivedNumericType.txt string.

Equations

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

source

def Unicode.derivedGeneralCategoryStr:

String

Includes the DerivedGeneralCategory.txt string.

Equations

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

source

def Unicode.derivedNumericValuesStr:

String

Includes the DerivedNumericValues.txt string.

Equations

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

Unihan Subdirectory #

source

def Unicode.unihanDictionaryIndicesStr:

String

Includes the Unihan_DictionaryIndices.txt string.

Equations

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

source

def Unicode.unihanOtherMappingsStr:

String

Includes the Unihan_OtherMappings.txt string.

Equations

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

source

def Unicode.unihanDictionaryLikeDataStr:

String

Includes the Unihan_DictionaryLikeData.txt string.

Equations

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

source

def Unicode.unihanRadicalStrokeCountsStr:

String

Includes the Unihan_RadicalStrokeCounts.txt string.

Equations

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

source

def Unicode.unihanIRGSourcesStr:

String

Includes the Unihan_IRGSources.txt string.

Equations

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

source

def Unicode.unihanReadingsStr:

String

Includes the Unihan_Readings.txt string.

Equations

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

source

def Unicode.unihanNumericValuesStr:

String

Includes the Unihan_NumericValues.txt string.

Equations

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

source

def Unicode.unihanVariantsStr:

String

Includes the Unihan_Variants.txt string.

Equations

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

HashMap Thunks #

source

instance Unicode.instHashableChar:

Hashable Char

Make Char Hashable as key of HashMap.

Equations

Unicode.instHashableChar = { hash := fun c => String.hash (toString c) }

source

def Unicode.parseStrToMapFn (s : String) (unit : Unit) :

Std.HashMap Char (List String)

Parse data file String into HashMap, the unit in parameter is left for Thunk.

Equations

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

source

def Unicode.parseStrToMapFn.lineCleanup (line : String) :

Option String

Remove comments and empty lines.

Equations

Unicode.parseStrToMapFn.lineCleanup line = Option.filter (fun a => decide (String.trim a ≠ "")) (List.head? (String.splitOn line "#"))

UCD Main Directory #

source

def Unicode.arabicShapingMap:

Thunk (Std.HashMap Char (List String))

Includes the ArabicShaping.txt data.

Equations

Unicode.arabicShapingMap = { fn := Unicode.parseStrToMapFn Unicode.arabicShapingStr }

source

def Unicode.bidiBracketsMap:

Thunk (Std.HashMap Char (List String))

Includes the BidiBrackets.txt data.

Equations

Unicode.bidiBracketsMap = { fn := Unicode.parseStrToMapFn Unicode.bidiBracketsStr }

source

def Unicode.bidiMirroringMap:

Thunk (Std.HashMap Char (List String))

Includes the BidiMirroring.txt data.

Equations

Unicode.bidiMirroringMap = { fn := Unicode.parseStrToMapFn Unicode.bidiMirroringStr }

source

def Unicode.normalizationCorrectionsMap:

Thunk (Std.HashMap Char (List String))

Includes the NormalizationCorrections.txt data.

Equations

Unicode.normalizationCorrectionsMap = { fn := Unicode.parseStrToMapFn Unicode.normalizationCorrectionsStr }

source

def Unicode.blocksMap:

Thunk (Std.HashMap Char (List String))

Includes the Blocks.txt data.

Equations

Unicode.blocksMap = { fn := Unicode.parseStrToMapFn Unicode.blocksStr }

source

def Unicode.nushuSourcesMap:

Thunk (Std.HashMap Char (List String))

Includes the NushuSources.txt data.

Equations

Unicode.nushuSourcesMap = { fn := Unicode.parseStrToMapFn Unicode.nushuSourcesStr }

source

def Unicode.propListMap:

Thunk (Std.HashMap Char (List String))

Includes the PropList.txt data.

Equations

Unicode.propListMap = { fn := Unicode.parseStrToMapFn Unicode.propListStr }

source

def Unicode.caseFoldingMap:

Thunk (Std.HashMap Char (List String))

Includes the CaseFolding.txt data.

Equations

Unicode.caseFoldingMap = { fn := Unicode.parseStrToMapFn Unicode.caseFoldingStr }

source

def Unicode.compositionExclusionsMap:

Thunk (Std.HashMap Char (List String))

Includes the CompositionExclusions.txt data.

Equations

Unicode.compositionExclusionsMap = { fn := Unicode.parseStrToMapFn Unicode.compositionExclusionsStr }

source

def Unicode.derivedAgeMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedAge.txt data.

Equations

Unicode.derivedAgeMap = { fn := Unicode.parseStrToMapFn Unicode.derivedAgeStr }

source

def Unicode.scriptExtensionsMap:

Thunk (Std.HashMap Char (List String))

Includes the ScriptExtensions.txt data.

Equations

Unicode.scriptExtensionsMap = { fn := Unicode.parseStrToMapFn Unicode.scriptExtensionsStr }

source

def Unicode.derivedCorePropertiesMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedCoreProperties.txt data.

Equations

Unicode.derivedCorePropertiesMap = { fn := Unicode.parseStrToMapFn Unicode.derivedCorePropertiesStr }

source

def Unicode.scriptsMap:

Thunk (Std.HashMap Char (List String))

Includes the Scripts.txt data.

Equations

Unicode.scriptsMap = { fn := Unicode.parseStrToMapFn Unicode.scriptsStr }

source

def Unicode.derivedNormalizationPropsMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedNormalizationProps.txt data.

Equations

Unicode.derivedNormalizationPropsMap = { fn := Unicode.parseStrToMapFn Unicode.derivedNormalizationPropsStr }

source

def Unicode.specialCasingMap:

Thunk (Std.HashMap Char (List String))

Includes the SpecialCasing.txt data.

Equations

Unicode.specialCasingMap = { fn := Unicode.parseStrToMapFn Unicode.specialCasingStr }

source

def Unicode.eastAsianWidthMap:

Thunk (Std.HashMap Char (List String))

Includes the EastAsianWidth.txt data.

Equations

Unicode.eastAsianWidthMap = { fn := Unicode.parseStrToMapFn Unicode.eastAsianWidthStr }

source

def Unicode.equivalentUnifiedIdeographMap:

Thunk (Std.HashMap Char (List String))

Includes the EquivalentUnifiedIdeograph.txt data.

Equations

Unicode.equivalentUnifiedIdeographMap = { fn := Unicode.parseStrToMapFn Unicode.equivalentUnifiedIdeographStr }

source

def Unicode.hangulSyllableTypeMap:

Thunk (Std.HashMap Char (List String))

Includes the HangulSyllableType.txt data.

Equations

Unicode.hangulSyllableTypeMap = { fn := Unicode.parseStrToMapFn Unicode.hangulSyllableTypeStr }

source

def Unicode.unicodeDataMap:

Thunk (Std.HashMap Char (List String))

Includes the UnicodeData.txt data. See unicodeDataMap.

Equations

Unicode.unicodeDataMap = { fn := Unicode.parseStrToMapFn Unicode.unicodeDataStr }

source

def Unicode.indicPositionalCategoryMap:

Thunk (Std.HashMap Char (List String))

Includes the IndicPositionalCategory.txt data.

Equations

Unicode.indicPositionalCategoryMap = { fn := Unicode.parseStrToMapFn Unicode.indicPositionalCategoryStr }

source

def Unicode.verticalOrientationMap:

Thunk (Std.HashMap Char (List String))

Includes the VerticalOrientation.txt data.

Equations

Unicode.verticalOrientationMap = { fn := Unicode.parseStrToMapFn Unicode.verticalOrientationStr }

source

def Unicode.indicSyllabicCategoryMap:

Thunk (Std.HashMap Char (List String))

Includes the IndicSyllabicCategory.txt data.

Equations

Unicode.indicSyllabicCategoryMap = { fn := Unicode.parseStrToMapFn Unicode.indicSyllabicCategoryStr }

source

def Unicode.jamoMap:

Thunk (Std.HashMap Char (List String))

Includes the Jamo.txt data.

Equations

Unicode.jamoMap = { fn := Unicode.parseStrToMapFn Unicode.jamoStr }

source

def Unicode.lineBreakMap:

Thunk (Std.HashMap Char (List String))

Includes the LineBreak.txt data.

Equations

Unicode.lineBreakMap = { fn := Unicode.parseStrToMapFn Unicode.lineBreakStr }

source

def Unicode.nameAliasesMap:

Thunk (Std.HashMap Char (List String))

Includes the NameAliases.txt data.

Equations

Unicode.nameAliasesMap = { fn := Unicode.parseStrToMapFn Unicode.nameAliasesStr }

Auxiliary Subdirectory #

source

def Unicode.graphemeBreakPropertyMap:

Thunk (Std.HashMap Char (List String))

Includes the GraphemeBreakProperty.txt data.

Equations

Unicode.graphemeBreakPropertyMap = { fn := Unicode.parseStrToMapFn Unicode.graphemeBreakPropertyStr }

source

def Unicode.wordBreakPropertyMap:

Thunk (Std.HashMap Char (List String))

Includes the WordBreakProperty.txt data.

Equations

Unicode.wordBreakPropertyMap = { fn := Unicode.parseStrToMapFn Unicode.wordBreakPropertyStr }

source

def Unicode.sentenceBreakPropertyMap:

Thunk (Std.HashMap Char (List String))

Includes the SentenceBreakProperty.txt data.

Equations

Unicode.sentenceBreakPropertyMap = { fn := Unicode.parseStrToMapFn Unicode.sentenceBreakPropertyStr }

Emoji Subdirectory #

source

def Unicode.emojiDataMap:

Thunk (Std.HashMap Char (List String))

Includes the emoji-data.txt data.

Equations

Unicode.emojiDataMap = { fn := Unicode.parseStrToMapFn Unicode.emojiDataStr }

Extracted Subdirectory #

source

def Unicode.derivedBidiClassMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedBidiClass.txt string.

Equations

Unicode.derivedBidiClassMap = { fn := Unicode.parseStrToMapFn Unicode.derivedBidiClassStr }

source

def Unicode.derivedJoiningGroupMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedJoiningGroup.txt string.

Equations

Unicode.derivedJoiningGroupMap = { fn := Unicode.parseStrToMapFn Unicode.derivedJoiningGroupStr }

source

def Unicode.derivedBinaryPropertiesMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedBinaryProperties.txt string.

Equations

Unicode.derivedBinaryPropertiesMap = { fn := Unicode.parseStrToMapFn Unicode.derivedBinaryPropertiesStr }

source

def Unicode.derivedJoiningTypeMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedJoiningType.txt string.

Equations

Unicode.derivedJoiningTypeMap = { fn := Unicode.parseStrToMapFn Unicode.derivedJoiningTypeStr }

source

def Unicode.derivedCombiningClassMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedCombiningClass.txt string.

Equations

Unicode.derivedCombiningClassMap = { fn := Unicode.parseStrToMapFn Unicode.derivedCombiningClassStr }

source

def Unicode.derivedLineBreakMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedLineBreak.txt string.

Equations

Unicode.derivedLineBreakMap = { fn := Unicode.parseStrToMapFn Unicode.derivedLineBreakStr }

source

def Unicode.derivedDecompositionTypeMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedDecompositionType.txt string.

Equations

Unicode.derivedDecompositionTypeMap = { fn := Unicode.parseStrToMapFn Unicode.derivedDecompositionTypeStr }

source

def Unicode.derivedNameMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedName.txt string.

Equations

Unicode.derivedNameMap = { fn := Unicode.parseStrToMapFn Unicode.derivedNameStr }

source

def Unicode.derivedEastAsianWidthMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedEastAsianWidth.txt string.

Equations

Unicode.derivedEastAsianWidthMap = { fn := Unicode.parseStrToMapFn Unicode.derivedEastAsianWidthStr }

source

def Unicode.derivedNumericTypeMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedNumericType.txt string.

Equations

Unicode.derivedNumericTypeMap = { fn := Unicode.parseStrToMapFn Unicode.derivedNumericTypeStr }

source

def Unicode.derivedGeneralCategoryMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedGeneralCategory.txt string.

Equations

Unicode.derivedGeneralCategoryMap = { fn := Unicode.parseStrToMapFn Unicode.derivedGeneralCategoryStr }

source

def Unicode.derivedNumericValuesMap:

Thunk (Std.HashMap Char (List String))

Includes the DerivedNumericValues.txt string.

Equations

Unicode.derivedNumericValuesMap = { fn := Unicode.parseStrToMapFn Unicode.derivedNumericValuesStr }

Unihan Subdirectory #

source

def Unicode.unihanDictionaryIndicesMap:

Thunk (Std.HashMap Char (List String))

Includes the Unihan_DictionaryIndices.txt string.

Equations

Unicode.unihanDictionaryIndicesMap = { fn := Unicode.parseStrToMapFn Unicode.unihanDictionaryIndicesStr }

source

def Unicode.unihanOtherMappingsMap:

Thunk (Std.HashMap Char (List String))

Includes the Unihan_OtherMappings.txt string.

Equations

Unicode.unihanOtherMappingsMap = { fn := Unicode.parseStrToMapFn Unicode.unihanOtherMappingsStr }

source

def Unicode.unihanDictionaryLikeDataMap:

Thunk (Std.HashMap Char (List String))

Includes the Unihan_DictionaryLikeData.txt string.

Equations

Unicode.unihanDictionaryLikeDataMap = { fn := Unicode.parseStrToMapFn Unicode.unihanDictionaryLikeDataStr }

source

def Unicode.unihanRadicalStrokeCountsMap:

Thunk (Std.HashMap Char (List String))

Includes the Unihan_RadicalStrokeCounts.txt string.

Equations

Unicode.unihanRadicalStrokeCountsMap = { fn := Unicode.parseStrToMapFn Unicode.unihanRadicalStrokeCountsStr }

source

def Unicode.unihanIRGSourcesMap:

Thunk (Std.HashMap Char (List String))

Includes the Unihan_IRGSources.txt string.

Equations

Unicode.unihanIRGSourcesMap = { fn := Unicode.parseStrToMapFn Unicode.unihanIRGSourcesStr }

source

def Unicode.unihanReadingsMap:

Thunk (Std.HashMap Char (List String))

Includes the Unihan_Readings.txt string.

Equations

Unicode.unihanReadingsMap = { fn := Unicode.parseStrToMapFn Unicode.unihanReadingsStr }

source

def Unicode.unihanNumericValuesMap:

Thunk (Std.HashMap Char (List String))

Includes the Unihan_NumericValues.txt string.

Equations

Unicode.unihanNumericValuesMap = { fn := Unicode.parseStrToMapFn Unicode.unihanNumericValuesStr }

source

def Unicode.unihanVariantsMap:

Thunk (Std.HashMap Char (List String))

Includes the Unihan_Variants.txt string.

Equations

Unicode.unihanVariantsMap = { fn := Unicode.parseStrToMapFn Unicode.unihanVariantsStr }