German case

This file defines the German cases and the forms of a German case paradigm. German has four cases, the nominative, the accusative, the genitive and the dative. The noun itself shows little of them: a regular noun adds -(e)s in the genitive singular of the masculine and the neuter and -n in the dative plural, and nothing else. Case is marked chiefly on the determiners and the adjectives of the noun phrase, together with its gender and number, as Durrell describes (German.Determiners, German.Adjectives). Blake gives the system as the four-case stage of his hierarchy.

Main definitions

• German.Case, German.Case.label: the four cases, and the comparative value each is named for.
• German.Case.forms: the forms of the four in the order of the school paradigms.

References

• [Dur11]
• [Bla94b]

inductive German.Case : Type

The four cases, in the order of the school paradigms.

• nom : Case

  The nominative.

• acc : Case

  The accusative.

• gen : Case

  The genitive.

• dat : Case

  The dative.

@[instance_reducible]

instance German.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance German.instFintypeCase : Fintype Case

Equations

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

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

Equations

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

@[instance_reducible]

instance German.instReprCase : Repr Case

Equations

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

def German.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• German.Case.nom.label = Case.nom
• German.Case.acc.label = Case.acc
• German.Case.gen.label = Case.gen
• German.Case.dat.label = Case.dat

def German.Case.forms {α : Type u_1} (nom acc gen dat : α) : Case → α

forms nom acc gen dat assigns each case its form.

Equations

• German.Case.forms nom acc gen dat German.Case.nom = nom
• German.Case.forms nom acc gen dat German.Case.acc = acc
• German.Case.forms nom acc gen dat German.Case.gen = gen
• German.Case.forms nom acc gen dat German.Case.dat = dat