Akan determiner inventory

Textbook-consensus types for the Akan (Kwa, Niger-Congo) determiner system, with no analytical denotations. The inventory is uncontroversial across the Akan literature ([Amf10], [AM13b], [Owu22] Ch 2–3). Paper-specific denotations ([Sch13] strong-DEF, [Bom18] weak-DEF, [Owu22] skolem-CF for bí, etc.) live in Studies files that consume these entries.

Main declarations

• Akan.Determiners.Definite — bare NP vs. nó (the DEF marker).
• Akan.Determiners.Indefinite — bare NP vs. bí (the INDEF marker).

Implementation notes

The Akan DEF marker nó occurs both nominally and clausally ([Owu22] Ch 4); only the nominal use is typed here. Bare NPs appear under both definiteness values ([Owu22] Ch 2 on definite bare nouns; App. A on bare-noun kind/indefinite readings) — the bare constructor is shared between the two inductives to reflect this.

inductive Akan.Determiners.Definite : Type

Akan adnominal definiteness contrast ([Owu22] Ch 2).

• bare : Definite

  Bare NP — definiteness inferred from context.

• no : Definite

  nó — postnominal DEF marker. Cross-categorial: also occurs on VPs and TPs ([AM13b], [Owu22] Ch 4).

@[implicit_reducible]

instance Akan.Determiners.instDecidableEqDefinite : DecidableEq Definite

Equations

• Akan.Determiners.instDecidableEqDefinite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Akan.Determiners.instReprDefinite.repr : Definite → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Akan.Determiners.instReprDefinite : Repr Definite

Equations

• Akan.Determiners.instReprDefinite = { reprPrec := Akan.Determiners.instReprDefinite.repr }

inductive Akan.Determiners.Indefinite : Type

Akan adnominal indefiniteness contrast ([Owu22] Ch 3).

• bare : Indefinite

  Bare NP — indefiniteness inferred from context.

• bi : Indefinite

  bí — postnominal INDEF marker.

@[implicit_reducible]

instance Akan.Determiners.instDecidableEqIndefinite : DecidableEq Indefinite

Equations

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

def Akan.Determiners.instReprIndefinite.repr : Indefinite → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Akan.Determiners.instReprIndefinite : Repr Indefinite

Equations

• Akan.Determiners.instReprIndefinite = { reprPrec := Akan.Determiners.instReprIndefinite.repr }