Latin case

The traditional description of Latin has six cases: nominative, vocative, accusative, genitive, dative and ablative. The vocative is a form of address standing outside the clause, and it is distinct from the nominative only in the singular of non-neuter second-declension nouns (Latin.Declension).

The ablative continues three cases that were once distinct, an ablative, a locative and an instrumental, and it expresses source, location and instrument accordingly. A separate locative survives for names of towns and a few nouns such as domī 'at home'. The goal of motion is expressed by the accusative, there being no allative. Blake takes Latin as his running example of an inflectional case system.

Main declarations

• Latin.Case: the six cases, in the order of the school paradigms.
• Latin.Case.label, Latin.Case.functions: the comparative value each case is named for, and the values it expresses.

References

• [Bla94b]

inductive Latin.Case : Type

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

• nom : Case

  The nominative.

• voc : Case

  The vocative.

• acc : Case

  The accusative.

• gen : Case

  The genitive.

• dat : Case

  The dative.

• abl : Case

  The ablative.

@[instance_reducible]

instance Latin.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Latin.instFintypeCase : Fintype Case

Equations

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

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

Equations

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

@[instance_reducible]

instance Latin.instReprCase : Repr Case

Equations

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

def Latin.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Latin.Case.nom.label = Case.nom
• Latin.Case.voc.label = Case.voc
• Latin.Case.acc.label = Case.acc
• Latin.Case.gen.label = Case.gen
• Latin.Case.dat.label = Case.dat
• Latin.Case.abl.label = Case.abl

def Latin.Case.functions : Case → Finset _root_.Case

The comparative values a case expresses: the accusative also expresses the goal of motion, and the ablative location and instrument as well as source.

Equations

• Latin.Case.acc.functions = {Case.acc, Case.all}
• Latin.Case.abl.functions = {Case.abl, Case.loc, Case.inst}
• x✝.functions = {x✝.label}

theorem Latin.Case.label_mem_functions (c : Case) : c.label ∈ c.functions