Russian case

This file defines the Russian cases, the six the Slavic languages share. [Tim93] (p. 836) takes Russian to have "six primary cases and two secondary cases (second genitive and second locative), the secondary cases being available for a decreasing number of masculines", and finds the historical vocative moribund. The cases here are the six primary ones; the secondary cases have forms of their own in some masculines only, and are left out.

References

• [Tim93]

inductive Russian.Case : Type

The six Russian cases.

• nom : Case

  The nominative.

• acc : Case

  The accusative.

• gen : Case

  The genitive.

• dat : Case

  The dative.

• inst : Case

  The instrumental.

• loc : Case

  The locative.

@[instance_reducible]

instance Russian.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Russian.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Russian.instReprCase : Repr Case

Equations

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

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

Equations

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

def Russian.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Russian.Case.nom.label = Case.nom
• Russian.Case.acc.label = Case.acc
• Russian.Case.gen.label = Case.gen
• Russian.Case.dat.label = Case.dat
• Russian.Case.inst.label = Case.inst
• Russian.Case.loc.label = Case.loc