def Fragments.Korean.Pronouns.na : Core.Pronouns.PronounEntry

나 na — 1sg plain.

Equations

• Fragments.Korean.Pronouns.na = { form := "na", person := some UD.Person.first, number := some Number.sg, script := some "나" }

def Fragments.Korean.Pronouns.jeo : Core.Pronouns.PronounEntry

저 jeo — 1sg humble.

Equations

• Fragments.Korean.Pronouns.jeo = { form := "jeo", person := some UD.Person.first, number := some Number.sg, register := Core.Register.Level.formal, script := some "저" }

def Fragments.Korean.Pronouns.uri : Core.Pronouns.PronounEntry

우리 uri — 1pl.

Equations

• Fragments.Korean.Pronouns.uri = { form := "uri", person := some UD.Person.first, number := some Number.pl, script := some "우리" }

def Fragments.Korean.Pronouns.neo : Core.Pronouns.PronounEntry

너 neo — 2sg plain.

Equations

• Fragments.Korean.Pronouns.neo = { form := "neo", person := some UD.Person.second, number := some Number.sg, script := some "너" }

def Fragments.Korean.Pronouns.dangsin : Core.Pronouns.PronounEntry

당신 dangsin — 2sg polite.

Equations

• Fragments.Korean.Pronouns.dangsin = { form := "dangsin", person := some UD.Person.second, number := some Number.sg, register := Core.Register.Level.formal, script := some "당신" }

def Fragments.Korean.Pronouns.geu : Core.Pronouns.PronounEntry

그 geu — 3sg masculine.

Equations

• Fragments.Korean.Pronouns.geu = { form := "geu", person := some UD.Person.third, number := some Number.sg, script := some "그" }

def Fragments.Korean.Pronouns.geunyeo : Core.Pronouns.PronounEntry

그녀 geunyeo — 3sg feminine.

Equations

• Fragments.Korean.Pronouns.geunyeo = { form := "geunyeo", person := some UD.Person.third, number := some Number.sg, script := some "그녀" }

def Fragments.Korean.Pronouns.geudeul : Core.Pronouns.PronounEntry

그들 geudeul — 3pl.

Equations

• Fragments.Korean.Pronouns.geudeul = { form := "geudeul", person := some UD.Person.third, number := some Number.pl, script := some "그들" }

def Fragments.Korean.Pronouns.secondPersonPronouns : List Core.Pronouns.PronounEntry

Equations

• Fragments.Korean.Pronouns.secondPersonPronouns = [Fragments.Korean.Pronouns.neo, Fragments.Korean.Pronouns.dangsin]

def Fragments.Korean.Pronouns.allPronouns : List Core.Pronouns.PronounEntry

Equations

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

def Fragments.Korean.Pronouns.yo : Core.Pronouns.AllocutiveEntry

-yo polite particle.

Equations

• Fragments.Korean.Pronouns.yo = { form := "-yo", register := Core.Register.Level.neutral, gloss := "POL" }

def Fragments.Korean.Pronouns.supnida : Core.Pronouns.AllocutiveEntry

-(su)pnida formal particle.

Equations

• Fragments.Korean.Pronouns.supnida = { form := "-(su)pnida", register := Core.Register.Level.formal, gloss := "FORM" }

def Fragments.Korean.Pronouns.allAllocParticles : List Core.Pronouns.AllocutiveEntry

Equations

• Fragments.Korean.Pronouns.allAllocParticles = [Fragments.Korean.Pronouns.yo, Fragments.Korean.Pronouns.supnida]

structure Fragments.Korean.Pronouns.VerbForm : Type

A verb form showing speech-level inflection.

• form : String
• gloss : String
• register : Core.Register.Level

instance Fragments.Korean.Pronouns.instReprVerbForm : Repr VerbForm

Equations

• Fragments.Korean.Pronouns.instReprVerbForm = { reprPrec := Fragments.Korean.Pronouns.instReprVerbForm.repr }

def Fragments.Korean.Pronouns.instReprVerbForm.repr : VerbForm → ℕ → Std.Format

Equations

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

def Fragments.Korean.Pronouns.instBEqVerbForm.beq : VerbForm → VerbForm → Bool

Equations

• Fragments.Korean.Pronouns.instBEqVerbForm.beq { form := a, gloss := a_1, register := a_2 } { form := b, gloss := b_1, register := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Fragments.Korean.Pronouns.instBEqVerbForm.beq x✝¹ x✝ = false

instance Fragments.Korean.Pronouns.instBEqVerbForm : BEq VerbForm

Equations

• Fragments.Korean.Pronouns.instBEqVerbForm = { beq := Fragments.Korean.Pronouns.instBEqVerbForm.beq }

def Fragments.Korean.Pronouns.ga : VerbForm

가 ga — "go" (plain/intimate).

Equations

• Fragments.Korean.Pronouns.ga = { form := "ga", gloss := "go.PLN", register := Core.Register.Level.informal }

def Fragments.Korean.Pronouns.gayo : VerbForm

가요 gayo — "go" (polite).

Equations

• Fragments.Korean.Pronouns.gayo = { form := "gayo", gloss := "go.POL", register := Core.Register.Level.neutral }

def Fragments.Korean.Pronouns.gamnida : VerbForm

갑니다 gamnida — "go" (formal).

Equations

• Fragments.Korean.Pronouns.gamnida = { form := "gamnida", gloss := "go.FORM", register := Core.Register.Level.formal }

theorem Fragments.Korean.Pronouns.has_all_persons : (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.first) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.third) = true

All three persons are attested.

theorem Fragments.Korean.Pronouns.has_both_numbers : (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.number == some Number.sg) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.number == some Number.pl) = true

Both singular and plural are attested.

theorem Fragments.Korean.Pronouns.first_person_humble : na.register = Core.Register.Level.informal ∧ jeo.register = Core.Register.Level.formal

1st person has plain/humble register distinction.

theorem Fragments.Korean.Pronouns.second_person_all_2p : (secondPersonPronouns.all fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true

2nd person pronouns are all second person.

theorem Fragments.Korean.Pronouns.tv_distinction : (secondPersonPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.register == Core.Register.Level.informal) = true ∧ (secondPersonPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.register == Core.Register.Level.formal) = true

The T/V register distinction is present in 2nd person.

theorem Fragments.Korean.Pronouns.verb_three_levels : ga.register = Core.Register.Level.informal ∧ gayo.register = Core.Register.Level.neutral ∧ gamnida.register = Core.Register.Level.formal

Verb forms span all three speech levels.