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 Syllable

Equations

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

source

instance Unicode.Hangul.instReprSyllable :

Repr Syllable

Equations

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

source

instance Unicode.Hangul.instInhabitedSyllable :

Inhabited Syllable

Equations

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

source

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, ⋯⟩

Instances For

source

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⟩

Instances For

source

@[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]

Instances For

source

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)

Instances For

source

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)

Instances For

source

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)

Instances For

source

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))

Instances For

source

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.

Instances For

source

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.

Instances For