Belarusian case

This file defines the Belarusian cases, the six the Slavic languages share. "Modern standard Belorussian has two numbers, six cases and three genders", and "The vocative case can no longer be regarded as a living category in the standard language, which has only the remnants божа/boža from бог/boh 'god' (as an exclamation) and браце/brace from брат/brat 'brother', дружа/druža from друг/druh 'friend' and сынку/synku (with stress shift) from сынок/synók 'son' (as modes of address)" ([May93], p. 900).

References

• [May93]

inductive Belarusian.Case : Type

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

Equations

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

@[instance_reducible]

instance Belarusian.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Belarusian.instReprCase : Repr Case

Equations

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

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

Equations

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

def Belarusian.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Belarusian.Case.nom.label = Case.nom
• Belarusian.Case.acc.label = Case.acc
• Belarusian.Case.gen.label = Case.gen
• Belarusian.Case.dat.label = Case.dat
• Belarusian.Case.inst.label = Case.inst
• Belarusian.Case.loc.label = Case.loc