Bantu noun classes

This file defines the types shared by the Bantu noun-class fragments: the semantic cores a gender may bear, [human], [animal] and [inanimate], or the [non-human] of a two-way system, and the status of a gender as interpretable, bearing a core, or uninterpretable, purely formal ([Car26]). Each language's fragment pairs its singular and plural classes into genders ([Car91]) and records the status of each gender.

References

• [Car91]
• [Car26]

inductive Bantu.SemanticCore : Type

A semantic core is the salient class of entities a gender is associated with. Xhosa has [human], [animal] and [inanimate], Shona [human] and [non-human].

• human : SemanticCore
• animal : SemanticCore
• inanimate : SemanticCore
• nonhuman : SemanticCore

@[instance_reducible]

instance Bantu.instDecidableEqSemanticCore : DecidableEq SemanticCore

Equations

• Bantu.instDecidableEqSemanticCore x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bantu.instReprSemanticCore : Repr SemanticCore

Equations

• Bantu.instReprSemanticCore = { reprPrec := Bantu.instReprSemanticCore.repr }

def Bantu.instReprSemanticCore.repr : SemanticCore → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Bantu.instReprSemanticCore.repr Bantu.SemanticCore.human prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bantu.SemanticCore.human")).group prec✝
• Bantu.instReprSemanticCore.repr Bantu.SemanticCore.animal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bantu.SemanticCore.animal")).group prec✝

inductive Bantu.GenderStatus : Type

A gender is interpretable, bearing a semantic core, or uninterpretable, with no association to a class of entities.

• interpretable : SemanticCore → GenderStatus
• uninterpretable : GenderStatus

@[instance_reducible]

instance Bantu.instDecidableEqGenderStatus : DecidableEq GenderStatus

Equations

• Bantu.instDecidableEqGenderStatus = Bantu.instDecidableEqGenderStatus.decEq

def Bantu.instDecidableEqGenderStatus.decEq (x✝ x✝¹ : GenderStatus) : Decidable (x✝ = x✝¹)

Equations

• Bantu.instDecidableEqGenderStatus.decEq (Bantu.GenderStatus.interpretable a) (Bantu.GenderStatus.interpretable b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Bantu.instDecidableEqGenderStatus.decEq (Bantu.GenderStatus.interpretable a) Bantu.GenderStatus.uninterpretable = isFalse ⋯
• Bantu.instDecidableEqGenderStatus.decEq Bantu.GenderStatus.uninterpretable (Bantu.GenderStatus.interpretable a) = isFalse ⋯
• Bantu.instDecidableEqGenderStatus.decEq Bantu.GenderStatus.uninterpretable Bantu.GenderStatus.uninterpretable = isTrue ⋯

@[instance_reducible]

instance Bantu.instReprGenderStatus : Repr GenderStatus

Equations

• Bantu.instReprGenderStatus = { reprPrec := Bantu.instReprGenderStatus.repr }

def Bantu.instReprGenderStatus.repr : GenderStatus → Nat → Std.Format

Equations

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