Czech case

This file defines the seven Czech cases: "The full seven cases survive" (Short, p. 465). About half the singular noun paradigms have a vocative "shared by no other case", and "no adjectival, pronominal, numeral or plural noun paradigms have distinct vocative forms (vocative = nominative)" (p. 465). A singular noun paradigm without a distinct vocative may share it with a case other than the nominative, as muži 'man' and stroji 'machine' do with the dative and the locative (p. 466).

References

• [Sho93a]

inductive Czech.Case : Type

The seven Czech 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 Czech.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Czech.instFintypeCase : Fintype Case

Equations

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

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

Equations

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

@[instance_reducible]

instance Czech.instReprCase : Repr Case

Equations

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

def Czech.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

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