Polish case

This file defines the seven Polish cases: "Polish has preserved the full inherited case system, including the vocative, but there is a growing tendency to use the nominative instead of the vocative for personal names. The vocative is consistently used with titles and with personal names when they are used as part of a vocative phrase" ([Rot93], p. 696), as in panie Janku and kochana Basiu 'dear Basia'.

References

• [Rot93]

inductive Polish.Case : Type

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

Equations

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

@[instance_reducible]

instance Polish.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Polish.instReprCase : Repr Case

Equations

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

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

Equations

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

def Polish.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

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