Ancient Greek case #

Ancient Greek has five cases: nominative, vocative, accusative, genitive and dative. Its dative does not correspond closely to the Latin dative. Greek has no ablative, and of the functions of the Latin ablative the genitive expresses source, while the dative expresses location and instrument beside the indirect object, so that the Greek dative is the more comprehensive case. Blake gives the system, vocative aside, as the four-case stage of his hierarchy.

Main declarations #

Greek.Ancient.Case: the five cases.
Greek.Ancient.Case.label, Greek.Ancient.Case.functions: the comparative value each case is named for, and the values it expresses.

References #

[Bla94b]

source

inductive Greek.Ancient.Case :

Type

The five cases.

nom : Case
The nominative.
voc : Case
The vocative.
acc : Case
The accusative.
gen : Case
The genitive.
dat : Case
The dative.

Instances For

source

@[instance_reducible]

instance Greek.Ancient.instDecidableEqCase :

DecidableEq Case

Equations

Greek.Ancient.instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[instance_reducible]

instance Greek.Ancient.instFintypeCase :

Fintype Case

Equations

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

source

@[instance_reducible]

instance Greek.Ancient.instReprCase :

Repr Case

Equations

Greek.Ancient.instReprCase = { reprPrec := Greek.Ancient.instReprCase.repr }

source

def Greek.Ancient.instReprCase.repr :

Case → ℕ → Std.Format

Equations

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