Sorbian cases

This file defines the cases of Upper and of Lower Sorbian: "Upper Sorbian has seven cases (nominative, vocative, accusative, genitive, dative, instrumental and locative). Lower Sorbian, having lost the vocative, has only six cases" ([Sto93b], p. 614). Even in Upper Sorbian only masculine nouns have a separate vocative form, and only in the singular, save mać 'mother', vocative maći. In both languages the instrumental has lost its prepositionless function.

References

• [Sto93b]

inductive Sorbian.Upper.Case : Type

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

Equations

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

@[instance_reducible]

instance Sorbian.Upper.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Sorbian.Upper.instReprCase : Repr Case

Equations

• Sorbian.Upper.instReprCase = { reprPrec := Sorbian.Upper.instReprCase.repr }

def Sorbian.Upper.instReprCase.repr : Case → ℕ → Std.Format

Equations

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

def Sorbian.Upper.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

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

inductive Sorbian.Lower.Case : Type

The six Lower Sorbian 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 Sorbian.Lower.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Sorbian.Lower.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Sorbian.Lower.instReprCase : Repr Case

Equations

• Sorbian.Lower.instReprCase = { reprPrec := Sorbian.Lower.instReprCase.repr }

def Sorbian.Lower.instReprCase.repr : Case → ℕ → Std.Format

Equations

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

def Sorbian.Lower.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Sorbian.Lower.Case.nom.label = Case.nom
• Sorbian.Lower.Case.acc.label = Case.acc
• Sorbian.Lower.Case.gen.label = Case.gen
• Sorbian.Lower.Case.dat.label = Case.dat
• Sorbian.Lower.Case.inst.label = Case.inst
• Sorbian.Lower.Case.loc.label = Case.loc