Hausa determiner inventory

Textbook-consensus types for the Hausa (Chadic) determiner system, with no analytical denotations. Sources: [New00] §17.5, §20, §21 and [Jag01] §9.5, §12.3. Paper-specific denotations (Q_∀ + ONE decomposition, choice-function vs. ∃-quantifier analysis of wani, etc.) live in Studies files that consume these entries.

Main declarations

• Hausa.UniversalQuantifier — the two morphologically distinct Hausa universal quantifiers.
• Hausa.Indefinite — bare vs. wani-series.

Implementation notes

The kō-wh universal is morphologically productive — kō + any of the wh-determiners from the wa- paradigm (Newman §21 Table 2, Jaggar §9.5.1 Table 24). The UniversalQuantifier.kowWh constructor abstracts over this productivity rather than enumerating each surface form.

inductive Hausa.UniversalQuantifier : Type

The two morphologically distinct Hausa adnominal universal quantifiers ([New00] §17.5; [Jag01] §9.5).

• kowWh : UniversalQuantifier

  kō-+wh productive paradigm: kōwā 'everyone', kōmē 'everything', kōwānè / kōwàcè / kōwàdànnè 'every X (m./f./pl.)', kō'inā 'everywhere', kōyàushē 'always'. Singulative- distributive: quantifies the individual members of the NP set unit-by-unit ([Jag01] §9.5.1 p.370).

• duk : UniversalQuantifier

  DUK 'all', allomorphs duk and dukà. Collective "single set" scope; does not inflect for gender or number; can quantify SG count, PL count, or mass NPs ([Jag01] §9.5.4 p.376).

@[implicit_reducible]

instance Hausa.instDecidableEqUniversalQuantifier : DecidableEq UniversalQuantifier

Equations

• Hausa.instDecidableEqUniversalQuantifier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Hausa.instReprUniversalQuantifier : Repr UniversalQuantifier

Equations

• Hausa.instReprUniversalQuantifier = { reprPrec := Hausa.instReprUniversalQuantifier.repr }

def Hausa.instReprUniversalQuantifier.repr : UniversalQuantifier → Nat → Std.Format

Equations

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

inductive Hausa.Indefinite : Type

The two Hausa adnominal indefinite strategies ([Jag01] §12.3).

• bare : Indefinite

  Bare NP indefinite.

• wani : Indefinite

  wani (m.) / wata (f.) / wa(dan)su (pl.), the marked indefinite determiner from the wa-paradigm ([New00] §21.1 row 8).

@[implicit_reducible]

instance Hausa.instDecidableEqIndefinite : DecidableEq Indefinite

Equations

• Hausa.instDecidableEqIndefinite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Hausa.instReprIndefinite : Repr Indefinite

Equations

• Hausa.instReprIndefinite = { reprPrec := Hausa.instReprIndefinite.repr }

def Hausa.instReprIndefinite.repr : Indefinite → Nat → Std.Format

Equations

• Hausa.instReprIndefinite.repr Hausa.Indefinite.bare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Indefinite.bare")).group prec✝
• Hausa.instReprIndefinite.repr Hausa.Indefinite.wani prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Indefinite.wani")).group prec✝