UnicodeBasic.Hangul

source

def Unicode.Hangul.Syllable.size :

Nat

Number of Hangul syllables

Equations

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

Instances For

source

def Unicode.Hangul.Syllable.base :

UInt32

Starting code point for Hangul syllables

Equations

Unicode.Hangul.Syllable.base = 44032

Instances For

source

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⟩ } }

Instances For

source

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)

Instances For

source

instance Unicode.Hangul.instDecidableEqSyllable :

DecidableEq Unicode.Hangul.Syllable

Equations

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

source

instance Unicode.Hangul.instReprSyllable :

Repr Unicode.Hangul.Syllable

Equations

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

source

instance Unicode.Hangul.instInhabitedSyllable :

Inhabited Unicode.Hangul.Syllable

Equations

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

source

def Unicode.Hangul.Syllable.toLV :

Unicode.Hangul.Syllable → Fin Unicode.Hangul.sizeLV

LV part of syllable

Equations

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

Instances For

source

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

Fin Unicode.Hangul.Syllable.size

Equations

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

Instances For

source

@[inline]

def Unicode.Hangul.Syllable.getShortName (s : Unicode.Hangul.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]

Instances For

source

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

Char

Get L part character for syllable

Equations

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

Instances For

source

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

Char

Get V part character for syllable

Equations

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

Instances For

source

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

Char

Get LV part character for syllable

Equations

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

Instances For

source

def Unicode.Hangul.Syllable.getTChar? (s : Unicode.Hangul.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))

Instances For

source

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

Option Unicode.Hangul.Syllable

Get Hangul syllable from code point

Equations

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

Instances For

source

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

Unicode.Hangul.Syllable

Get Hangul syllable from code point

Equations

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

Instances For