Bayso noun number

Bayso nouns have a general form outside the number system, non-committal as to how many, and within the system a singular, a paucal for two to about six, and a plural, each with its own suffix; nouns fall into two genders. An agreeing verb has three forms only, labelled from the pronouns, which distinguish a masculine and a feminine singular and one plural: general and singular nouns take their gender's form, paucal nouns the plural form, and plural nouns the masculine one, as Hayward, Corbett and Hayward, and Corbett describe.

References

• R. J. Hayward, Bayso revisited: some preliminary linguistic observations, II (1979)
• G. G. Corbett, R. J. Hayward, Gender and number in Bayso (1987)
• G. G. Corbett, Number (2000)

inductive Bayso.Gender : Type

The two genders.

• masc : Gender
• fem : Gender

@[instance_reducible]

instance Bayso.instDecidableEqGender : DecidableEq Gender

Equations

• Bayso.instDecidableEqGender x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bayso.instReprGender.repr : Gender → ℕ → Std.Format

Equations

• Bayso.instReprGender.repr Bayso.Gender.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Gender.masc")).group prec✝
• Bayso.instReprGender.repr Bayso.Gender.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Gender.fem")).group prec✝

@[instance_reducible]

instance Bayso.instReprGender : Repr Gender

Equations

• Bayso.instReprGender = { reprPrec := Bayso.instReprGender.repr }

@[instance_reducible]

instance Bayso.instFintypeGender : Fintype Gender

Equations

• Bayso.instFintypeGender = { elems := { val := ↑Bayso.Gender.enumList, nodup := Bayso.Gender.enumList_nodup }, complete := Bayso.instFintypeGender._proof_1 }

def Bayso.numberSystem : Number.System

Bayso nouns have a singular, a paucal and a plural, and a general number outside the system.

Equations

• Bayso.numberSystem = { values := {Number.singular, Number.paucal, Number.plural}, hasGeneral := true }

def Bayso.nounNumbers : Finset Number

The numbers a noun has a form for, the general and the values of the system.

Equations

• Bayso.nounNumbers = insert Number.general Bayso.numberSystem.values

def Bayso.pronounNumberSystem : Number.System

Pronouns distinguish the singular and the plural.

Equations

• Bayso.pronounNumberSystem = Number.System.singularPlural

inductive Bayso.Concord : Type

The three forms of an agreeing verb, labelled from the pronouns that take them: hudure 'slept' masculine, hudurte feminine, hudureene plural.

• masc : Concord
• fem : Concord
• plural : Concord

@[instance_reducible]

instance Bayso.instDecidableEqConcord : DecidableEq Concord

Equations

• Bayso.instDecidableEqConcord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bayso.instReprConcord.repr : Concord → ℕ → Std.Format

Equations

• Bayso.instReprConcord.repr Bayso.Concord.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Concord.masc")).group prec✝
• Bayso.instReprConcord.repr Bayso.Concord.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Concord.fem")).group prec✝
• Bayso.instReprConcord.repr Bayso.Concord.plural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Concord.plural")).group prec✝

@[instance_reducible]

instance Bayso.instReprConcord : Repr Concord

Equations

• Bayso.instReprConcord = { reprPrec := Bayso.instReprConcord.repr }

@[instance_reducible]

instance Bayso.instFintypeConcord : Fintype Concord

Equations

• Bayso.instFintypeConcord = { elems := { val := ↑Bayso.Concord.enumList, nodup := Bayso.Concord.enumList_nodup }, complete := Bayso.instFintypeConcord._proof_1 }

def Bayso.Gender.pronounConcord (g : Gender) : ↥pronounNumberSystem.values → Concord

A pronoun takes its gender's concord in the singular and the plural concord in the plural.

Equations

• Bayso.Gender.masc.pronounConcord = Bayso.pronounNumberSystem.elim Bayso.Concord.masc Bayso.Concord.plural Bayso.Gender.pronounConcord._proof_3
• Bayso.Gender.fem.pronounConcord = Bayso.pronounNumberSystem.elim Bayso.Concord.fem Bayso.Concord.plural Bayso.Gender.pronounConcord._proof_3

def Bayso.Gender.concord : Gender → ↥nounNumbers → Concord

A noun takes its gender's concord in the general and the singular, the plural concord in the paucal, and the masculine concord in the plural.

Equations

• Bayso.Gender.masc.concord ⟨Number.general, property⟩ = Bayso.Concord.masc
• Bayso.Gender.masc.concord ⟨Number.singular, property⟩ = Bayso.Concord.masc
• Bayso.Gender.fem.concord ⟨Number.general, property⟩ = Bayso.Concord.fem
• Bayso.Gender.fem.concord ⟨Number.singular, property⟩ = Bayso.Concord.fem
• x✝.concord ⟨Number.paucal, property⟩ = Bayso.Concord.plural
• x✝.concord ⟨Number.plural, property⟩ = Bayso.Concord.masc
• x✝.concord ⟨Number.dual, h⟩ = absurd h Bayso.Gender.concord._proof_3
• x✝.concord ⟨Number.trial, h⟩ = absurd h Bayso.Gender.concord._proof_4
• x✝.concord ⟨Number.greaterPaucal, h⟩ = absurd h Bayso.Gender.concord._proof_5
• x✝.concord ⟨Number.greaterPlural, h⟩ = absurd h Bayso.Gender.concord._proof_6
• x✝.concord ⟨Number.minimal, h⟩ = absurd h Bayso.Gender.concord._proof_7
• x✝.concord ⟨Number.augmented, h⟩ = absurd h Bayso.Gender.concord._proof_8
• x✝.concord ⟨Number.unitAugmented, h⟩ = absurd h Bayso.Gender.concord._proof_9
• x✝.concord ⟨Number.globalPlural, h⟩ = absurd h Bayso.Gender.concord._proof_10

@[simp]

theorem Bayso.Gender.concord_general (g : Gender) : g.concord ⟨Number.general, concord_general._proof_1⟩ = g.concord ⟨Number.singular, concord_general._proof_2⟩

@[simp]

theorem Bayso.Gender.concord_paucal (g : Gender) : g.concord ⟨Number.paucal, concord_paucal._proof_1⟩ = Concord.plural

@[simp]

theorem Bayso.Gender.concord_plural (g : Gender) : g.concord ⟨Number.plural, concord_plural._proof_1⟩ = Concord.masc

structure Bayso.Nounextends GenderedNoun Bayso.Gender : Type

A noun with its four number forms; the citation form is the general one.

• form : String
• gloss : String
• gender : Bayso.Gender
• referentGender : Option ReferentGender
• singular : String

  The singular form.

• paucal : String

  The paucal form.

• plural : String

  The plural form.

def Bayso.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Bayso.instDecidableEqNoun : DecidableEq Noun

Equations

• Bayso.instDecidableEqNoun = Bayso.instDecidableEqNoun.decEq

@[instance_reducible]

instance Bayso.instReprNoun : Repr Noun

Equations

• Bayso.instReprNoun = { reprPrec := Bayso.instReprNoun.repr }

def Bayso.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

def Bayso.luban : Noun

lúban 'lion'.

Equations

• Bayso.luban = { form := "lúban", gloss := "lion", gender := Bayso.Gender.masc, singular := "lubántiti", paucal := "lubanjaa", plural := "lubanjool" }

def Bayso.kimbir : Noun

kimbír 'bird'.

Equations

• Bayso.kimbir = { form := "kimbír", gloss := "bird", gender := Bayso.Gender.fem, singular := "kimbírtiti", paucal := "kimbirjaa", plural := "kimbirjool" }

def Bayso.allNouns : List Noun

The nouns the sources cite.

Equations

• Bayso.allNouns = [Bayso.luban, Bayso.kimbir]

def Bayso.Noun.formAt (n : Noun) : ↥nounNumbers → String

The form of a noun in each number.

Equations

• n.formAt ⟨Number.general, property⟩ = n.form
• n.formAt ⟨Number.singular, property⟩ = n.singular
• n.formAt ⟨Number.paucal, property⟩ = n.paucal
• n.formAt ⟨Number.plural, property⟩ = n.plural
• n.formAt ⟨Number.dual, h⟩ = absurd h Bayso.Gender.concord._proof_3
• n.formAt ⟨Number.trial, h⟩ = absurd h Bayso.Gender.concord._proof_4
• n.formAt ⟨Number.greaterPaucal, h⟩ = absurd h Bayso.Gender.concord._proof_5
• n.formAt ⟨Number.greaterPlural, h⟩ = absurd h Bayso.Gender.concord._proof_6
• n.formAt ⟨Number.minimal, h⟩ = absurd h Bayso.Gender.concord._proof_7
• n.formAt ⟨Number.augmented, h⟩ = absurd h Bayso.Gender.concord._proof_8
• n.formAt ⟨Number.unitAugmented, h⟩ = absurd h Bayso.Gender.concord._proof_9
• n.formAt ⟨Number.globalPlural, h⟩ = absurd h Bayso.Gender.concord._proof_10