Latvian case

Latvian has seven cases, the nominative, genitive, dative, accusative, instrumental, locative and vocative, encoded by endings ([KL21] §2.1.4, p. 104). The instrumental has become homonymous with the accusative in the singular and with the dative in the plural, and only the preposition ar 'with' tells them apart (p. 118). It is the standard example of a case value with no form of its own, kept so that a preposition governs one case whatever the number ([Cor15] §3.6).

Main definitions

• Latvian.Case, Latvian.Case.label: the seven cases, and the comparative value each is named for.

References

• [KL21]
• [Cor15]

inductive Latvian.Case : Type

The seven cases.

• nom : Case

  The nominative.

• gen : Case

  The genitive.

• dat : Case

  The dative.

• acc : Case

  The accusative.

• inst : Case

  The instrumental, the case the preposition ar 'with' governs.

• loc : Case

  The locative.

• voc : Case

  The vocative.

@[instance_reducible]

instance Latvian.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Latvian.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Latvian.instReprCase : Repr Case

Equations

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

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

Equations

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

def Latvian.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

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