def Basque.Pronouns.ni : PersonalPronoun

ni — 1sg.

Equations

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

def Basque.Pronouns.gu : PersonalPronoun

gu — 1pl.

Equations

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

def Basque.Pronouns.hi : PersonalPronoun

hi — 2sg familiar (T form).

Equations

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

def Basque.Pronouns.zu : PersonalPronoun

zu — 2sg formal (V form).

Equations

• Basque.Pronouns.zu = { form := "zu", person := some Person.second, number := some Number.singular, register := Features.Register.Level.formal }

def Basque.Pronouns.zuek : PersonalPronoun

zuek — 2pl.

Equations

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

def Basque.Pronouns.hura : PersonalPronoun

hura — 3sg.

Equations

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

def Basque.Pronouns.haiek : PersonalPronoun

haiek — 3pl.

Equations

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

def Basque.Pronouns.secondPersonPronouns : List PersonalPronoun

Equations

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

def Basque.Pronouns.allPronouns : List PersonalPronoun

Equations

• Basque.Pronouns.allPronouns = [Basque.Pronouns.ni, Basque.Pronouns.gu] ++ Basque.Pronouns.secondPersonPronouns ++ [Basque.Pronouns.zuek, Basque.Pronouns.hura, Basque.Pronouns.haiek]

def Basque.Pronouns.allocFamiliar : Pronoun.AllocutiveEntry

-n familiar allocutive suffix.

Equations

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

def Basque.Pronouns.allocFormal : Pronoun.AllocutiveEntry

-zu formal allocutive suffix.

Equations

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

def Basque.Pronouns.allAllocMarkers : List Pronoun.AllocutiveEntry

Equations

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

structure Basque.Pronouns.VerbForm : Type

A verb form showing allocutive inflection.

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

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

Equations

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

@[implicit_reducible]

instance Basque.Pronouns.instReprVerbForm : Repr VerbForm

Equations

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

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

Equations

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

@[implicit_reducible]

instance Basque.Pronouns.instBEqVerbForm : BEq VerbForm

Equations

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

def Basque.Pronouns.duk : VerbForm

duk — "you have" (familiar).

Equations

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

def Basque.Pronouns.duzu : VerbForm

duzu — "you have" (formal).

Equations

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

theorem Basque.Pronouns.has_all_persons : (allPronouns.any fun (x : PersonalPronoun) => x.person == some Person.first) = true ∧ (allPronouns.any fun (x : PersonalPronoun) => x.person == some Person.second) = true ∧ (allPronouns.any fun (x : PersonalPronoun) => x.person == some Person.third) = true

All three persons are attested.

theorem Basque.Pronouns.has_both_numbers : (allPronouns.any fun (x : PersonalPronoun) => x.number == some Number.singular) = true ∧ (allPronouns.any fun (x : PersonalPronoun) => x.number == some Number.plural) = true

Both singular and plural are attested.

theorem Basque.Pronouns.second_person_all_2p : (secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

2nd person pronouns are all second person.

theorem Basque.Pronouns.tv_distinction : (secondPersonPronouns.any fun (x : PersonalPronoun) => x.register == Features.Register.Level.informal) = true ∧ (secondPersonPronouns.any fun (x : PersonalPronoun) => x.register == Features.Register.Level.formal) = true

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

theorem Basque.Pronouns.verb_register_matches_pronouns : duk.register = hi.register ∧ duzu.register = zu.register

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