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 ([hayward-1979]; [corbett-hayward-1987]; [Cor00]).

References

• [R. J. Hayward, Bayso revisited: some preliminary linguistic observations, II (1979)][hayward-1979]
• [G. G. Corbett, R. J. Hayward, Gender and number in Bayso (1987)][corbett-hayward-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 ⋯

@[instance_reducible]

instance Bayso.instReprGender : Repr Gender

Equations

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

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.instFintypeGender : Fintype Gender

Equations

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

inductive Bayso.Value : Type

The four numbers of a noun: the general outside the system, and singular, paucal and plural within it.

• general : Value
• singular : Value
• paucal : Value
• plural : Value

@[instance_reducible]

instance Bayso.instDecidableEqValue : DecidableEq Value

Equations

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

def Bayso.instReprValue.repr : Value → ℕ → Std.Format

Equations

• Bayso.instReprValue.repr Bayso.Value.general prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Value.general")).group prec✝
• Bayso.instReprValue.repr Bayso.Value.singular prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Value.singular")).group prec✝
• Bayso.instReprValue.repr Bayso.Value.paucal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Value.paucal")).group prec✝
• Bayso.instReprValue.repr Bayso.Value.plural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bayso.Value.plural")).group prec✝

@[instance_reducible]

instance Bayso.instReprValue : Repr Value

Equations

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

@[instance_reducible]

instance Bayso.instFintypeValue : Fintype Value

Equations

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

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 ⋯

@[instance_reducible]

instance Bayso.instReprConcord : Repr Concord

Equations

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

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.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 : Gender → Bool → Concord

The concord a pronoun takes: its gender in the singular, the plural form in the plural.

Equations

• Bayso.Gender.masc.pronounConcord false = Bayso.Concord.masc
• Bayso.Gender.fem.pronounConcord false = Bayso.Concord.fem
• x✝.pronounConcord true = Bayso.Concord.plural

def Bayso.Gender.concord : Gender → Value → Concord

The concord a noun takes, by gender and number: its gender's form for the general and the singular, the plural form for the paucal, the masculine form for the plural.

Equations

• Bayso.Gender.masc.concord Bayso.Value.general = Bayso.Concord.masc
• Bayso.Gender.masc.concord Bayso.Value.singular = Bayso.Concord.masc
• Bayso.Gender.fem.concord Bayso.Value.general = Bayso.Concord.fem
• Bayso.Gender.fem.concord Bayso.Value.singular = Bayso.Concord.fem
• x✝.concord Bayso.Value.paucal = Bayso.Concord.plural
• x✝.concord Bayso.Value.plural = Bayso.Concord.masc

@[simp]

theorem Bayso.Gender.concord_general (g : Gender) : g.concord Value.general = g.concord Value.singular

General and singular nouns take their gender's concord.

@[simp]

theorem Bayso.Gender.concord_paucal (g : Gender) : g.concord Value.paucal = Concord.plural

Paucal nouns take the plural concord.

@[simp]

theorem Bayso.Gender.concord_plural (g : Gender) : g.concord Value.plural = Concord.masc

Plural nouns take the masculine concord.

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
• isNaturalGender : Bool
• 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

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

Equations

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

@[instance_reducible]

instance Bayso.instReprNoun : Repr Noun

Equations

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

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) : Value → String

The form of a noun in each number.

Equations

• n.formAt Bayso.Value.general = n.form
• n.formAt Bayso.Value.singular = n.singular
• n.formAt Bayso.Value.paucal = n.paucal
• n.formAt Bayso.Value.plural = n.plural