Nez Perce case

This file defines the cases of the Nez Perce relative-pronoun paradigm, the nominative, the ergative and the accusative ([Dea16], reproduced in [Dea26] (22)).

Implementation notes

The cases are the three of the paradigm; the other cases of the language are not recorded.

References

• [Dea16]
• [Dea26]

inductive NezPerce.Case : Type

The cases of the relative-pronoun paradigm.

• nom : Case

  The nominative.

• erg : Case

  The ergative.

• acc : Case

  The accusative.

@[instance_reducible]

instance NezPerce.instDecidableEqCase : DecidableEq Case

Equations

• NezPerce.instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NezPerce.instFintypeCase : Fintype Case

Equations

• NezPerce.instFintypeCase = { elems := { val := ↑NezPerce.Case.enumList, nodup := NezPerce.Case.enumList_nodup }, complete := NezPerce.instFintypeCase._proof_1 }

@[instance_reducible]

instance NezPerce.instReprCase : Repr Case

Equations

• NezPerce.instReprCase = { reprPrec := NezPerce.instReprCase.repr }

def NezPerce.instReprCase.repr : Case → ℕ → Std.Format

Equations

• NezPerce.instReprCase.repr NezPerce.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NezPerce.Case.nom")).group prec✝
• NezPerce.instReprCase.repr NezPerce.Case.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NezPerce.Case.erg")).group prec✝
• NezPerce.instReprCase.repr NezPerce.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "NezPerce.Case.acc")).group prec✝

def NezPerce.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• NezPerce.Case.nom.label = Case.nom
• NezPerce.Case.erg.label = Case.erg
• NezPerce.Case.acc.label = Case.acc