def Fragments.Basque.Pronouns.ni : Core.Pronouns.PronounEntry

ni — 1sg.

Equations

• Fragments.Basque.Pronouns.ni = { form := "ni", person := some UD.Person.first, number := some Number.sg }

def Fragments.Basque.Pronouns.gu : Core.Pronouns.PronounEntry

gu — 1pl.

Equations

• Fragments.Basque.Pronouns.gu = { form := "gu", person := some UD.Person.first, number := some Number.pl }

def Fragments.Basque.Pronouns.hi : Core.Pronouns.PronounEntry

hi — 2sg familiar (T form).

Equations

• Fragments.Basque.Pronouns.hi = { form := "hi", person := some UD.Person.second, number := some Number.sg }

def Fragments.Basque.Pronouns.zu : Core.Pronouns.PronounEntry

zu — 2sg formal (V form).

Equations

• Fragments.Basque.Pronouns.zu = { form := "zu", person := some UD.Person.second, number := some Number.sg, register := Core.Register.Level.formal }

def Fragments.Basque.Pronouns.zuek : Core.Pronouns.PronounEntry

zuek — 2pl.

Equations

• Fragments.Basque.Pronouns.zuek = { form := "zuek", person := some UD.Person.second, number := some Number.pl }

def Fragments.Basque.Pronouns.hura : Core.Pronouns.PronounEntry

hura — 3sg.

Equations

• Fragments.Basque.Pronouns.hura = { form := "hura", person := some UD.Person.third, number := some Number.sg }

def Fragments.Basque.Pronouns.haiek : Core.Pronouns.PronounEntry

haiek — 3pl.

Equations

• Fragments.Basque.Pronouns.haiek = { form := "haiek", person := some UD.Person.third, number := some Number.pl }

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

Equations

• Fragments.Basque.Pronouns.secondPersonPronouns = [Fragments.Basque.Pronouns.hi, Fragments.Basque.Pronouns.zu]

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

Equations

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

def Fragments.Basque.Pronouns.allocFamiliar : Core.Pronouns.AllocutiveEntry

-n familiar allocutive suffix.

Equations

• Fragments.Basque.Pronouns.allocFamiliar = { form := "-n", register := Core.Register.Level.informal, gloss := "2sg.familiar.alloc" }

def Fragments.Basque.Pronouns.allocFormal : Core.Pronouns.AllocutiveEntry

-zu formal allocutive suffix.

Equations

• Fragments.Basque.Pronouns.allocFormal = { form := "-zu", register := Core.Register.Level.formal, gloss := "2sg.formal.alloc" }

def Fragments.Basque.Pronouns.allAllocMarkers : List Core.Pronouns.AllocutiveEntry

Equations

• Fragments.Basque.Pronouns.allAllocMarkers = [Fragments.Basque.Pronouns.allocFamiliar, Fragments.Basque.Pronouns.allocFormal]

structure Fragments.Basque.Pronouns.VerbForm : Type

A verb form showing allocutive inflection.

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

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

Equations

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

instance Fragments.Basque.Pronouns.instReprVerbForm : Repr VerbForm

Equations

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

instance Fragments.Basque.Pronouns.instBEqVerbForm : BEq VerbForm

Equations

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

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

Equations

• Fragments.Basque.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.Basque.Pronouns.instBEqVerbForm.beq x✝¹ x✝ = false

def Fragments.Basque.Pronouns.duk : VerbForm

duk — "you have" (familiar).

Equations

• Fragments.Basque.Pronouns.duk = { form := "duk", gloss := "have.2sg.fam", register := Core.Register.Level.informal }

def Fragments.Basque.Pronouns.duzu : VerbForm

duzu — "you have" (formal).

Equations

• Fragments.Basque.Pronouns.duzu = { form := "duzu", gloss := "have.2sg.for", register := Core.Register.Level.formal }

theorem Fragments.Basque.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.Basque.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.Basque.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.Basque.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.Basque.Pronouns.verb_register_matches_pronouns : duk.register = hi.register ∧ duzu.register = zu.register

Verb forms have matching register levels with 2nd person pronouns.