Swahili nouns

This file defines the Swahili nouns of Corbett's account of gender assignment. A noun carries a morphological class, the pair of classes whose prefixes it takes, and a controller gender, the pair of classes whose agreements it controls. The two coincide for most nouns and come apart for animates, which take the agreements of classes 1 and 2 whatever their prefix, as kifaru 'rhinoceros' with the prefix of class 7 and tembo 'elephant' with none. An augmentative moves a stem into classes 5/6 and a diminutive into 7/8, joka 'giant snake' and kijoka 'tiny snake' from nyoka 'snake'; the assignment rules that read these off are in Studies/Corbett1991.lean.

Main definitions

• Swahili.Noun: a noun with its morphological class, its animacy and its evaluative derivation
• Swahili.allNouns: the nouns of Corbett's examples and rules

References

• G. G. Corbett, Gender (1991)

inductive Swahili.Evaluative : Type

An evaluative derivation moves a stem into another class.

• augmentative : Evaluative

  Into classes 5/6.

• diminutive : Evaluative

  Into classes 7/8.

@[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 with its morphological class, the pair of classes whose prefixes it carries, the gender whose agreements it controls, and its animacy.

• form : String
• gloss : String
• gender : Swahili.Gender
• referentGender : Option ReferentGender
• morphClass : Gender

  The pair of classes whose prefixes the noun carries.

• animacy : Animacy

  The animacy of the noun's referents.

• 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

kikapu 'basket'.

Equations

• Swahili.kikapu = { form := "kikapu", gloss := "basket", gender := Swahili.Gender.genderD, morphClass := Swahili.Gender.genderD, animacy := Animacy.inanimate }

def Swahili.kiti : Noun

kiti 'stool'.

Equations

• Swahili.kiti = { form := "kiti", gloss := "stool", gender := Swahili.Gender.genderD, morphClass := Swahili.Gender.genderD, animacy := Animacy.inanimate }

def Swahili.mti : Noun

mti 'tree'.

Equations

• Swahili.mti = { form := "mti", gloss := "tree", gender := Swahili.Gender.genderB, morphClass := Swahili.Gender.genderB, animacy := Animacy.inanimate }

def Swahili.mguu : Noun

mguu 'leg'.

Equations

• Swahili.mguu = { form := "mguu", gloss := "leg", gender := Swahili.Gender.genderB, morphClass := Swahili.Gender.genderB, animacy := Animacy.inanimate }

def Swahili.nyumba : Noun

nyumba 'house'.

Equations

• Swahili.nyumba = { form := "nyumba", gloss := "house", gender := Swahili.Gender.genderE, morphClass := Swahili.Gender.genderE, animacy := Animacy.inanimate }

def Swahili.mtu : Noun

mtu 'person'.

Equations

• Swahili.mtu = { form := "mtu", gloss := "person", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderA, animacy := Animacy.human }

def Swahili.mwalimu : Noun

mwalimu 'teacher'.

Equations

• Swahili.mwalimu = { form := "mwalimu", gloss := "teacher", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderA, animacy := Animacy.human }

def Swahili.mnyama : Noun

mnyama 'animal'.

Equations

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

def Swahili.mdudu : Noun

mdudu 'insect'.

Equations

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

def Swahili.kifaru : Noun

kifaru 'rhinoceros', with the prefix of class 7 and the agreements of classes 1/2.

Equations

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

def Swahili.kiboko : Noun

kiboko 'hippopotamus', with the prefix of class 7 and the agreements of classes 1/2.

Equations

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

def Swahili.mjusi : Noun

mjusi 'lizard', with the prefix of class 3.

Equations

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

def Swahili.jogoo : Noun

jogoo 'rooster', of morphological class 5/6.

Equations

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

def Swahili.kipofu : Noun

kipofu 'blind person', with the prefix of class 7.

Equations

• Swahili.kipofu = { form := "kipofu", gloss := "blind person", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderD, animacy := Animacy.human }

def Swahili.tembo : Noun

tembo 'elephant', of morphological class 9/10.

Equations

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

def Swahili.nyoka : Noun

nyoka 'snake', of morphological class 9/10.

Equations

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

def Swahili.rafiki : Noun

rafiki 'friend', of morphological class 9/10.

Equations

• Swahili.rafiki = { form := "rafiki", gloss := "friend", gender := Swahili.Gender.genderA, morphClass := Swahili.Gender.genderE, animacy := Animacy.human }

def Swahili.ngombe : Noun

ng'ombe 'cow', of morphological class 9/10.

Equations

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

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

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

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

The nouns of Corbett's examples and rules.

Equations

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