Tamil case

Tamil has eight cases, the seven of Classical Armenian on Blake's inflectional case hierarchy, the nominative, accusative, genitive, dative, locative, ablative and instrumental, and the comitative, which Dravidian grammars call the sociative. The oblique cases of some singular nouns are suffixed to an oblique stem distinct from the nominative: maram 'tree' has the accusative maratt-ai and the dative maratt-ukku, and the stem-forming element never appears without a following case suffix, so that the nominative stands off from the other cases. Blake takes Tamil as the eight-case stage of his hierarchy (Studies/Blake1994.lean).

Main definitions

• Tamil.Case, Tamil.Case.label: the eight cases, and the comparative value each is named for.

References

• [Bla94b]

inductive Tamil.Case : Type

The eight cases.

• nom : Case

  The nominative.

• acc : Case

  The accusative.

• gen : Case

  The genitive.

• dat : Case

  The dative.

• loc : Case

  The locative.

• abl : Case

  The ablative.

• inst : Case

  The instrumental.

• com : Case

  The comitative.

@[instance_reducible]

instance Tamil.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Tamil.instFintypeCase : Fintype Case

Equations

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

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

Equations

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

@[instance_reducible]

instance Tamil.instReprCase : Repr Case

Equations

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

def Tamil.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Tamil.Case.nom.label = Case.nom
• Tamil.Case.acc.label = Case.acc
• Tamil.Case.gen.label = Case.gen
• Tamil.Case.dat.label = Case.dat
• Tamil.Case.loc.label = Case.loc
• Tamil.Case.abl.label = Case.abl
• Tamil.Case.inst.label = Case.inst
• Tamil.Case.com.label = Case.com