Chiquihuitlán Mazatec verb inflection

Two of the three cross-cutting inflection-class systems of Chiquihuitlán Mazatec verbs over the cells 1sg, 2sg, 3, 1incl, 1pl, 2pl, after Jamieson's description as tabulated in [AM13a]: the ten final-vowel classes and the six neutral-aspect tone patterns, each with unit weight.

References

• [AM13a]

@[reducible, inline]

abbrev Mazatec.Verbs.firstSg : Fin 6

The cells.

Equations

• Mazatec.Verbs.firstSg = 0

@[reducible, inline]

abbrev Mazatec.Verbs.secondSg : Fin 6

Equations

• Mazatec.Verbs.secondSg = 1

@[reducible, inline]

abbrev Mazatec.Verbs.third : Fin 6

Equations

• Mazatec.Verbs.third = 2

@[reducible, inline]

abbrev Mazatec.Verbs.firstIncl : Fin 6

Equations

• Mazatec.Verbs.firstIncl = 3

@[reducible, inline]

abbrev Mazatec.Verbs.firstPl : Fin 6

Equations

• Mazatec.Verbs.firstPl = 4

@[reducible, inline]

abbrev Mazatec.Verbs.secondPl : Fin 6

Equations

• Mazatec.Verbs.secondPl = 5

inductive Mazatec.Verbs.Vowel : Type

Final vowels, nasal ones suffixed N.

• ae : Vowel
• i : Vowel
• e : Vowel
• u : Vowel
• o : Vowel
• a : Vowel
• eN : Vowel
• iN : Vowel
• uN : Vowel
• oN : Vowel
• aN : Vowel

@[instance_reducible]

instance Mazatec.Verbs.instDecidableEqVowel : DecidableEq Vowel

Equations

• Mazatec.Verbs.instDecidableEqVowel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Mazatec.Verbs.instReprVowel : Repr Vowel

Equations

• Mazatec.Verbs.instReprVowel = { reprPrec := Mazatec.Verbs.instReprVowel.repr }

def Mazatec.Verbs.instReprVowel.repr : Vowel → ℕ → Std.Format

Equations

• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.ae prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.ae")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.i")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.e")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.u")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.o")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.a")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.eN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.eN")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.iN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.iN")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.uN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.uN")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.oN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.oN")).group prec✝
• Mazatec.Verbs.instReprVowel.repr Mazatec.Verbs.Vowel.aN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Vowel.aN")).group prec✝

def Mazatec.Verbs.finalVowels : Morphology.ParadigmSystem 6 Vowel

The ten final-vowel classes.

Equations

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

inductive Mazatec.Verbs.Tone : Type

Tone patterns, named by their tone numbers.

• t3_1 : Tone
• t3_31 : Tone
• t3_14 : Tone
• t1_1 : Tone
• t2_2 : Tone
• t2_24 : Tone
• t3_2 : Tone
• t1_43 : Tone
• t3_24 : Tone
• t14_42 : Tone
• t14_34 : Tone
• t14_3 : Tone

@[instance_reducible]

instance Mazatec.Verbs.instDecidableEqTone : DecidableEq Tone

Equations

• Mazatec.Verbs.instDecidableEqTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Mazatec.Verbs.instReprTone : Repr Tone

Equations

• Mazatec.Verbs.instReprTone = { reprPrec := Mazatec.Verbs.instReprTone.repr }

def Mazatec.Verbs.instReprTone.repr : Tone → ℕ → Std.Format

Equations

• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t3_1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t3_1")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t3_31 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t3_31")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t3_14 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t3_14")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t1_1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t1_1")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t2_2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t2_2")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t2_24 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t2_24")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t3_2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t3_2")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t1_43 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t1_43")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t3_24 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t3_24")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t14_42 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t14_42")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t14_34 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t14_34")).group prec✝
• Mazatec.Verbs.instReprTone.repr Mazatec.Verbs.Tone.t14_3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mazatec.Verbs.Tone.t14_3")).group prec✝

def Mazatec.Verbs.tones : Morphology.ParadigmSystem 6 Tone

The six neutral-aspect tone patterns.

Equations

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