Turkish case

This file defines the cases of Turkish. Göksel and Kerslake list five case suffixes, the accusative -(y)I, the dative -(y)A, the locative -DA, the ablative -DAn and the genitive -(n)In, and Blake's table adds the unmarked nominative for a system of six cases. The suffixes are the case exponents of the nominal in Morphotactics.lean, which maps each to the case it realizes and proves that they realize every case but the nominative, once each. The comitative and instrumental -(y)lA is not a case suffix in the grammar's analysis but an unstressable marker that forms postpositional phrases, Turkish.Adpositions.ile.

Main definitions

• Turkish.Case, Turkish.Case.label: the six cases, and the comparative value each is named for

References

• A. Göksel and C. Kerslake, Turkish: A Comprehensive Grammar (2005)
• B. J. Blake, Case (1994)

inductive Turkish.Case : Type

The six cases.

• nom : Case

  The nominative, unmarked.

• acc : Case

  The accusative.

• dat : Case

  The dative.

• loc : Case

  The locative.

• abl : Case

  The ablative.

• gen : Case

  The genitive.

@[instance_reducible]

instance Turkish.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Turkish.instFintypeCase : Fintype Case

Equations

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

@[instance_reducible]

instance Turkish.instReprCase : Repr Case

Equations

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

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

Equations

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

def Turkish.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Turkish.Case.nom.label = Case.nom
• Turkish.Case.acc.label = Case.acc
• Turkish.Case.dat.label = Case.dat
• Turkish.Case.loc.label = Case.loc
• Turkish.Case.abl.label = Case.abl
• Turkish.Case.gen.label = Case.gen