Hungarian case

Hungarian marks case by agglutinative suffix. Kenesei, Vago and Fenyvesi list eighteen cases: the nominative, the accusative -t, the dative -nak ~ -nek, the instrumental -val ~ -vel, the causal -ért, the essive -ul ~ -ül, the essive-formal -ként, the terminative -ig, the translative -vá ~ -vé, and the nine local cases, which form a matrix of three regions, interior, exterior and near, by three directions, motion toward, rest and motion away: the illative -ba ~ -be, inessive -ban ~ -ben and elative -ból ~ -ből, the sublative -ra ~ -re, superessive -n and delative -ról ~ -ről, and the allative -hoz, adessive -nál ~ -nél and ablative -tól ~ -től. Rounds adds the less productive temporal -kor, distributive -nként, distributive-temporal -nta and sociative -stul ~ -stül. There is no genitive: the possessor within the noun phrase is nominative or dative, and both grammars gloss -nak ~ -nek as a dative throughout, the reading under which Blake and Caha take Hungarian's missing genitive as a superficial exception to the case hierarchy.

Main definitions

• Hungarian.Case, Hungarian.Case.label: the cases with a comparative label, and that label.

Implementation notes

The essive-formal, the distributive, the distributive-temporal and the sociative have no comparative label and are left out; the instrumental -val ~ -vel also expresses accompaniment, and no separate comitative is recorded.

References

• [KVF98]
• [Rou01]
• [Cah08]

inductive Hungarian.Case : Type

The cases with a comparative label: the three grammatical cases, the nine local cases, the instrumental, the causal, the essive, the translative, the terminative and the temporal.

• nom : Case

  The nominative.

• acc : Case

  The accusative.

• dat : Case

  The dative.

• ine : Case

  The inessive.

• ade : Case

  The adessive.

• sup : Case

  The superessive.

• ela : Case

  The elative.

• abl : Case

  The ablative.

• del : Case

  The delative.

• ill : Case

  The illative.

• all : Case

  The allative.

• sub : Case

  The sublative.

• inst : Case

  The instrumental.

• caus : Case

  The causal.

• ess : Case

  The essive.

• transl : Case

  The translative.

• ter : Case

  The terminative.

• tem : Case

  The temporal.

@[instance_reducible]

instance Hungarian.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance Hungarian.instFintypeCase : Fintype Case

Equations

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

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

Equations

• Hungarian.instReprCase.repr Hungarian.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.nom")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.acc")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.dat")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.ine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.ine")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.ade prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.ade")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.sup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.sup")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.ela prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.ela")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.abl")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.del prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.del")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.ill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.ill")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.all")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.sub")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.inst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.inst")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.caus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.caus")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.ess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.ess")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.transl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.transl")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.ter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.ter")).group prec✝
• Hungarian.instReprCase.repr Hungarian.Case.tem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hungarian.Case.tem")).group prec✝

@[instance_reducible]

instance Hungarian.instReprCase : Repr Case

Equations

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

def Hungarian.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• Hungarian.Case.nom.label = Case.nom
• Hungarian.Case.acc.label = Case.acc
• Hungarian.Case.dat.label = Case.dat
• Hungarian.Case.ine.label = Case.ine
• Hungarian.Case.ade.label = Case.ade
• Hungarian.Case.sup.label = Case.sup
• Hungarian.Case.ela.label = Case.ela
• Hungarian.Case.abl.label = Case.abl
• Hungarian.Case.del.label = Case.del
• Hungarian.Case.ill.label = Case.ill
• Hungarian.Case.all.label = Case.all
• Hungarian.Case.sub.label = Case.sub
• Hungarian.Case.inst.label = Case.inst
• Hungarian.Case.caus.label = Case.caus
• Hungarian.Case.ess.label = Case.ess
• Hungarian.Case.transl.label = Case.transl
• Hungarian.Case.ter.label = Case.ter
• Hungarian.Case.tem.label = Case.tem