def Unicode.Hangul.shortNameL : Array String

Equations

• Unicode.Hangul.shortNameL = #["G", "GG", "N", "D", "DD", "R", "M", "B", "BB", "S", "SS", "", "J", "JJ", "C", "K", "T", "P", "H"]

def Unicode.Hangul.shortNameV : Array String

Equations

• Unicode.Hangul.shortNameV = #["A", "AE", "YA", "YAE", "EO", "E", "YEO", "YE", "O", "WA", "WAE", "OE", "YO", "U", "WEO", "WE", "WI", "YU", "EU", "YI", "I"]

def Unicode.Hangul.shortNameT : Array String

Equations

• Unicode.Hangul.shortNameT = #["", "G", "GG", "GS", "N", "NJ", "NH", "D", "L", "LG", "LM", "LB", "LS", "LT", "LP", "LH", "M", "B", "BS", "S", "SS", "NG", "J", "C", "K", "T", "P", "H"]

@[reducible, inline]

abbrev Unicode.Hangul.sizeL : Nat

Equations

• Unicode.Hangul.sizeL = Unicode.Hangul.shortNameL.size

@[reducible, inline]

abbrev Unicode.Hangul.sizeV : Nat

Equations

• Unicode.Hangul.sizeV = Unicode.Hangul.shortNameV.size

@[reducible, inline]

abbrev Unicode.Hangul.sizeT : Nat

Equations

• Unicode.Hangul.sizeT = Unicode.Hangul.shortNameT.size

@[reducible, inline]

abbrev Unicode.Hangul.sizeLV : Nat

Equations

• Unicode.Hangul.sizeLV = Unicode.Hangul.sizeL * Unicode.Hangul.sizeV

@[reducible, inline]

abbrev Unicode.Hangul.sizeVT : Nat

Equations

• Unicode.Hangul.sizeVT = Unicode.Hangul.sizeV * Unicode.Hangul.sizeT

@[reducible, inline]

abbrev Unicode.Hangul.sizeLVT : Nat

Equations

• Unicode.Hangul.sizeLVT = Unicode.Hangul.sizeL * Unicode.Hangul.sizeV * Unicode.Hangul.sizeT

@[reducible, inline]

abbrev Unicode.Hangul.baseL : UInt32

Equations

• Unicode.Hangul.baseL = 4352

@[reducible, inline]

abbrev Unicode.Hangul.baseV : UInt32

Equations

• Unicode.Hangul.baseV = 4449

@[reducible, inline]

abbrev Unicode.Hangul.baseT : UInt32

Equations

• Unicode.Hangul.baseT = 4519

def Unicode.Hangul.Syllable.size : Nat

Number of Hangul syllables

Equations

• Unicode.Hangul.Syllable.size = Unicode.Hangul.sizeLVT

def Unicode.Hangul.Syllable.base : UInt32

Starting code point for Hangul syllables

Equations

• Unicode.Hangul.Syllable.base = 44032

def Unicode.Hangul.Syllable.last : UInt32

Stopping code point for Hangul syllables

Equations

• Unicode.Hangul.Syllable.last = { toBitVec := { toFin := ⟨44032 + Unicode.Hangul.Syllable.size - 1, Unicode.Hangul.Syllable.last._proof_1✝⟩ } }

structure Unicode.Hangul.Syllable : Type

Hangul syllable type

• toL : Fin sizeL

  L part of syllable

• toV : Fin sizeV

  V part of syllable

• toT : Fin sizeT

  T part of syllable (0 means none)

@[implicit_reducible]

instance Unicode.Hangul.instDecidableEqSyllable : DecidableEq Syllable

Equations

• Unicode.Hangul.instDecidableEqSyllable = Unicode.Hangul.instDecidableEqSyllable.decEq

def Unicode.Hangul.instDecidableEqSyllable.decEq (x✝ x✝¹ : Syllable) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Unicode.Hangul.instReprSyllable : Repr Syllable

Equations

• Unicode.Hangul.instReprSyllable = { reprPrec := Unicode.Hangul.instReprSyllable.repr }

def Unicode.Hangul.instReprSyllable.repr : Syllable → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Unicode.Hangul.instInhabitedSyllable : Inhabited Syllable

Equations

• Unicode.Hangul.instInhabitedSyllable = { default := { toL := ⟨0, Unicode.Hangul.instInhabitedSyllable._proof_1⟩, toV := ⟨0, Unicode.Hangul.instInhabitedSyllable._proof_2⟩ } }

def Unicode.Hangul.Syllable.toLV : Syllable → Fin sizeLV

LV part of syllable

Equations

• { toL := ⟨l, hl⟩, toV := ⟨v, hv⟩, toT := toT }.toLV = ⟨l * Unicode.Hangul.sizeV + v, ⋯⟩

def Unicode.Hangul.Syllable.index (s : Syllable) : Fin size

Equations

• s.index = match s.toLV, s.toT with | ⟨lv, hlv⟩, ⟨t, ht⟩ => have this := ⋯; ⟨lv * Unicode.Hangul.sizeT + t, this⟩

@[inline]

def Unicode.Hangul.Syllable.getShortName (s : Syllable) : String

Get short name for Hangul syllable

Equations

• s.getShortName = Unicode.Hangul.shortNameL[s.toL] ++ Unicode.Hangul.shortNameV[s.toV] ++ Unicode.Hangul.shortNameT[s.toT]

def Unicode.Hangul.Syllable.getLChar (s : Syllable) : Char

Get L part character for syllable

Equations

• s.getLChar = Char.ofNat (Unicode.Hangul.baseL.toNat + ↑s.toL)

def Unicode.Hangul.Syllable.getVChar (s : Syllable) : Char

Get V part character for syllable

Equations

• s.getVChar = Char.ofNat (Unicode.Hangul.baseV.toNat + ↑s.toV)

def Unicode.Hangul.Syllable.getLVChar (s : Syllable) : Char

Get LV part character for syllable

Equations

• s.getLVChar = Char.ofNat (Unicode.Hangul.Syllable.base.toNat + Unicode.Hangul.sizeT * ↑s.toLV)

def Unicode.Hangul.Syllable.getTChar? (s : Syllable) : Option Char

Get T part character for syllable

Equations

• s.getTChar? = if (↑s.toT == 0) = true then none else pure (Char.ofNat (Unicode.Hangul.baseT.toNat + ↑s.toT))

def Unicode.Hangul.getSyllable? (code : UInt32) : Option Syllable

Get Hangul syllable from code point

Equations

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

def Unicode.Hangul.getSyllable! (code : UInt32) : Syllable

Get Hangul syllable from code point

Equations

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