Ukrainian case

This file defines the seven Ukrainian cases: "Ukrainian preserves the original set of cases: nominative, accusative, genitive, dative, instrumental and locative. In addition, the vocative is preserved even though the vocative singular in colloquial speech is occasionally replaced by the nominative and in the plural the vocative has no forms of its own, except in the word панове/panove 'gentlemen'" ([She93], p. 956).

References

• [She93]

inductive Ukrainian.Case : Type

The seven Ukrainian cases.

• nom : Case

  The nominative.

• voc : Case

  The vocative.

• acc : Case

  The accusative.

• gen : Case

  The genitive.

• dat : Case

  The dative.

• inst : Case

  The instrumental.

• loc : Case

  The locative.

@[instance_reducible]

instance Ukrainian.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Ukrainian.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Ukrainian.instReprCase : Repr Case

Equations

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

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

Equations

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

def Ukrainian.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Ukrainian.Case.nom.label = Case.nom
• Ukrainian.Case.voc.label = Case.voc
• Ukrainian.Case.acc.label = Case.acc
• Ukrainian.Case.gen.label = Case.gen
• Ukrainian.Case.dat.label = Case.dat
• Ukrainian.Case.inst.label = Case.inst
• Ukrainian.Case.loc.label = Case.loc