Mongolian case

Mongolian (Khalkha and Chakhar) has seven cases: nominative, accusative, genitive, dative, ablative, instrumental and comitative. The inventory has no dedicated locative, which postpositions express. [Gon22]'s account of how the structural cases are assigned is in Studies/Gong2022.lean.

References

• [Gon22]

inductive Mongolian.Case : Type

The seven cases.

• nom : Case

  The nominative.

• acc : Case

  The accusative.

• gen : Case

  The genitive.

• dat : Case

  The dative.

• abl : Case

  The ablative.

• inst : Case

  The instrumental.

• com : Case

  The comitative.

@[instance_reducible]

instance Mongolian.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Mongolian.instFintypeCase : Fintype Case

Equations

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

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

Equations

• Mongolian.instReprCase.repr Mongolian.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mongolian.Case.nom")).group prec✝
• Mongolian.instReprCase.repr Mongolian.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mongolian.Case.acc")).group prec✝
• Mongolian.instReprCase.repr Mongolian.Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mongolian.Case.gen")).group prec✝
• Mongolian.instReprCase.repr Mongolian.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mongolian.Case.dat")).group prec✝
• Mongolian.instReprCase.repr Mongolian.Case.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mongolian.Case.abl")).group prec✝
• Mongolian.instReprCase.repr Mongolian.Case.inst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mongolian.Case.inst")).group prec✝
• Mongolian.instReprCase.repr Mongolian.Case.com prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mongolian.Case.com")).group prec✝

@[instance_reducible]

instance Mongolian.instReprCase : Repr Case

Equations

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

def Mongolian.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Mongolian.Case.nom.label = Case.nom
• Mongolian.Case.acc.label = Case.acc
• Mongolian.Case.gen.label = Case.gen
• Mongolian.Case.dat.label = Case.dat
• Mongolian.Case.abl.label = Case.abl
• Mongolian.Case.inst.label = Case.inst
• Mongolian.Case.com.label = Case.com