Swahili nouns

Nouns carry a morphological class, the singular and plural prefixes they take, and a controller gender, the class pair whose agreements they control; the two coincide for most nouns but come apart for animates, which take class 1/2 agreements whatever their prefixes ([welmers-1973]; [Cor91]). Augmentatives and diminutives are formed by moving a stem into class 5/6 or 7/8.

References

• [W. E. Welmers, African Language Structures (1973)][welmers-1973]
• G. G. Corbett, Gender (1991)

inductive Swahili.Evaluative : Type

Evaluative derivation by class change.

• augmentative : Evaluative
• diminutive : Evaluative

@[instance_reducible]

instance Swahili.instDecidableEqEvaluative : DecidableEq Evaluative

Equations

• Swahili.instDecidableEqEvaluative x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Swahili.instReprEvaluative.repr : Evaluative → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Swahili.instReprEvaluative : Repr Evaluative

Equations

• Swahili.instReprEvaluative = { reprPrec := Swahili.instReprEvaluative.repr }

@[instance_reducible]

instance Swahili.instFintypeEvaluative : Fintype Evaluative

Equations

• Swahili.instFintypeEvaluative = { elems := { val := ↑Swahili.Evaluative.enumList, nodup := Swahili.Evaluative.enumList_nodup }, complete := Swahili.instFintypeEvaluative._proof_1 }

structure Swahili.Nounextends GenderedNoun Swahili.Gender : Type

A Swahili noun: its morphological class (the prefixes on the noun), the gender whose agreements it controls, and whether it denotes an animate.

• form : String
• gloss : String
• gender : Swahili.Gender
• isNaturalGender : Bool
• morphClass : Gender

  The class pair whose prefixes the noun carries.

• animate : Bool

  Whether the noun denotes an animate.

• evaluative : Option Evaluative

  Augmentative or diminutive derivation, if any.

@[instance_reducible]

instance Swahili.instDecidableEqNoun : DecidableEq Noun

Equations

• Swahili.instDecidableEqNoun = Swahili.instDecidableEqNoun.decEq

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

Equations

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

@[instance_reducible]

instance Swahili.instReprNoun : Repr Noun

Equations

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

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

Equations

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

def Swahili.kikapu : Noun

Equations

• Swahili.kikapu = { form := "kikapu", gloss := "basket", gender := Swahili.Gender.genderD, morphClass := Swahili.Gender.genderD, animate := false }

def Swahili.kiti : Noun

Equations

• Swahili.kiti = { form := "kiti", gloss := "stool", gender := Swahili.Gender.genderD, morphClass := Swahili.Gender.genderD, animate := false }

def Swahili.mti : Noun

Equations

• Swahili.mti = { form := "mti", gloss := "tree", gender := Swahili.Gender.genderB, morphClass := Swahili.Gender.genderB, animate := false }

def Swahili.mguu : Noun

Equations

• Swahili.mguu = { form := "mguu", gloss := "leg", gender := Swahili.Gender.genderB, morphClass := Swahili.Gender.genderB, animate := false }

def Swahili.nyumba : Noun

Equations

• Swahili.nyumba = { form := "nyumba", gloss := "house", gender := Swahili.Gender.genderE, morphClass := Swahili.Gender.genderE, animate := false }

def Swahili.mtu : Noun

Equations

• Swahili.mtu = { form := "mtu", gloss := "person", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderA, animate := true }

def Swahili.mwalimu : Noun

Equations

• Swahili.mwalimu = { form := "mwalimu", gloss := "teacher", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderA, animate := true }

def Swahili.mnyama : Noun

Equations

• Swahili.mnyama = { form := "mnyama", gloss := "animal", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderA, animate := true }

def Swahili.mdudu : Noun

Equations

• Swahili.mdudu = { form := "mdudu", gloss := "insect", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderA, animate := true }

def Swahili.kifaru : Noun

kifaru 'rhinoceros': class 7 prefix, class 1/2 agreements.

Equations

• Swahili.kifaru = { form := "kifaru", gloss := "rhinoceros", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderD, animate := true }

def Swahili.kiboko : Noun

kiboko 'hippopotamus': class 7 prefix, class 1/2 agreements.

Equations

• Swahili.kiboko = { form := "kiboko", gloss := "hippopotamus", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderD, animate := true }

def Swahili.mjusi : Noun

Equations

• Swahili.mjusi = { form := "mjusi", gloss := "lizard", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderB, animate := true }

def Swahili.jogoo : Noun

Equations

• Swahili.jogoo = { form := "jogoo", gloss := "rooster", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderC, animate := true }

def Swahili.kipofu : Noun

Equations

• Swahili.kipofu = { form := "kipofu", gloss := "blind person", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderD, animate := true }

def Swahili.tembo : Noun

Equations

• Swahili.tembo = { form := "tembo", gloss := "elephant", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderE, animate := true }

def Swahili.nyoka : Noun

Equations

• Swahili.nyoka = { form := "nyoka", gloss := "snake", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderE, animate := true }

def Swahili.rafiki : Noun

Equations

• Swahili.rafiki = { form := "rafiki", gloss := "friend", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderE, animate := true }

def Swahili.ngombe : Noun

Equations

• Swahili.ngombe = { form := "ng'ombe", gloss := "cow", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderE, animate := true }

def Swahili.joka : Noun

joka 'giant snake', the augmentative of nyoka.

Equations

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

def Swahili.kitoto : Noun

kitoto 'baby', the diminutive of mtoto 'child'.

Equations

• Swahili.kitoto = { form := "kitoto", gloss := "baby", gender := Swahili.Gender.genderD, morphClass := Swahili.Gender.genderD, animate := true, evaluative := some Swahili.Evaluative.diminutive }

def Swahili.kijoka : Noun

kijoka 'tiny snake', the diminutive of joka.

Equations

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

def Swahili.allNouns : List Noun

Equations

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

theorem Swahili.faithful_subjPrefix : Gender.Faithful fun (g : Gender) (pl : Bool) => (if pl = true then g.pluralClass else g.singularClass).subjPrefix

Verbal subject agreement, singular and plural, distinguishes the five genders.