def Fragments.Galician.Pronouns.eu : Typology.PronounEntry

eu — 1sg.

Equations

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

def Fragments.Galician.Pronouns.nos : Typology.PronounEntry

nós — 1pl.

Equations

• Fragments.Galician.Pronouns.nos = { form := "nós", person := some UD.Person.first, number := some Number.pl }

def Fragments.Galician.Pronouns.ti : Typology.PronounEntry

ti — 2sg familiar (T form).

Equations

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

def Fragments.Galician.Pronouns.vostede : Typology.PronounEntry

vostede — 2sg formal (V form).

Equations

• Fragments.Galician.Pronouns.vostede = { form := "vostede", person := some UD.Person.second, number := some Number.sg, register := Features.Register.Level.formal }

def Fragments.Galician.Pronouns.vos_pl : Typology.PronounEntry

vós — 2pl familiar.

Equations

• Fragments.Galician.Pronouns.vos_pl = { form := "vós", person := some UD.Person.second, number := some Number.pl }

def Fragments.Galician.Pronouns.vostedes : Typology.PronounEntry

vostedes — 2pl formal.

Equations

• Fragments.Galician.Pronouns.vostedes = { form := "vostedes", person := some UD.Person.second, number := some Number.pl, register := Features.Register.Level.formal }

def Fragments.Galician.Pronouns.el : Typology.PronounEntry

el — 3sg masculine.

Equations

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

def Fragments.Galician.Pronouns.ela : Typology.PronounEntry

ela — 3sg feminine.

Equations

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

def Fragments.Galician.Pronouns.eles : Typology.PronounEntry

eles — 3pl masculine.

Equations

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

def Fragments.Galician.Pronouns.elas : Typology.PronounEntry

elas — 3pl feminine.

Equations

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

def Fragments.Galician.Pronouns.secondPersonPronouns : List Typology.PronounEntry

Equations

• Fragments.Galician.Pronouns.secondPersonPronouns = [Fragments.Galician.Pronouns.ti, Fragments.Galician.Pronouns.vostede]

def Fragments.Galician.Pronouns.allPronouns : List Typology.PronounEntry

Equations

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

def Fragments.Galician.Pronouns.che : Typology.AllocutiveEntry

che — familiar dative clitic (2sg ethical dative).

Equations

• Fragments.Galician.Pronouns.che = { form := "che", register := Features.Register.Level.informal, gloss := "2sg.DAT.fam" }

def Fragments.Galician.Pronouns.allAllocClitics : List Typology.AllocutiveEntry

Equations

• Fragments.Galician.Pronouns.allAllocClitics = [Fragments.Galician.Pronouns.che]

structure Fragments.Galician.Pronouns.VerbForm : Type

A verb form with optional allocutive clitic.

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Galician.Pronouns.instReprVerbForm : Repr VerbForm

Equations

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Galician.Pronouns.instBEqVerbForm : BEq VerbForm

Equations

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

def Fragments.Galician.Pronouns.vas : VerbForm

vas — "you go" (familiar, can host che).

Equations

• Fragments.Galician.Pronouns.vas = { form := "vas", gloss := "go.2sg.fam", register := Features.Register.Level.informal }

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

All three persons are attested.

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

Both singular and plural are attested.

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

2nd person pronouns are all second person.

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

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

theorem Fragments.Galician.Pronouns.che_is_informal : che.register = Features.Register.Level.informal

The allocutive clitic che is informal-level.

theorem Fragments.Galician.Pronouns.plural_tv : vos_pl.register = Features.Register.Level.informal ∧ vostedes.register = Features.Register.Level.formal

2pl preserves the T/V distinction (vós fam / vostedes form).