Icelandic case

Icelandic has four cases, the nominative, the accusative, the dative and the genitive, in the order of the school paradigms, and its nouns, adjectives, articles and pronouns inflect for all four in both numbers, as Thráinsson's overview of the nominal inflection sets out. Subjects and objects alike bear all four: the verbs of Icelandic.Verbs record the case array of each, and every case is the case of some subject and of some object (Icelandic.Verbs.subject_cases, Icelandic.Verbs.object_cases). Blake gives the system as the four-case stage of his hierarchy, beside German's (Studies/Blake1994.lean).

Main definitions

• Icelandic.Case, Icelandic.Case.label: the four cases, and the comparative value each is named for.

References

• [Thr07]
• [Bla94b]

inductive Icelandic.Case : Type

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

• nom : Case

  The nominative.

• acc : Case

  The accusative.

• dat : Case

  The dative.

• gen : Case

  The genitive.

@[instance_reducible]

instance Icelandic.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Icelandic.instFintypeCase : Fintype Case

Equations

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

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

Equations

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

@[instance_reducible]

instance Icelandic.instReprCase : Repr Case

Equations

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

def Icelandic.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

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