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 Unicode.Hangul.sizeL✝

  L part of syllable

• toV : Fin Unicode.Hangul.sizeV✝

  V part of syllable

• toT : Fin Unicode.Hangul.sizeT✝

  T part of syllable (0 means none)

instance Unicode.Hangul.instDecidableEqSyllable : DecidableEq Syllable

Equations

• Unicode.Hangul.instDecidableEqSyllable = Unicode.Hangul.decEqSyllable✝

instance Unicode.Hangul.instReprSyllable : Repr Syllable

Equations

• Unicode.Hangul.instReprSyllable = { reprPrec := Unicode.Hangul.reprSyllable✝ }

instance Unicode.Hangul.instInhabitedSyllable : Inhabited Syllable

Equations

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

def Unicode.Hangul.Syllable.toLV : Syllable → Fin Unicode.Hangul.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⟩ => let_fun 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.