Case

The comparative case values, the concepts under which the case systems of different languages are compared. The cases of a language are its own categories and are not these values ([Has10]): a fragment defines them as an inductive type L.Case and matches them to the comparative values by two functions, L.Case.label, the value its traditional name corresponds to, and, where the grammar lists more than the name, L.Case.functions, the values it expresses ([Bla01] ch. 2). Where the grammar gives its forms, L.Case.exponents lists the morphs that mark it, allomorphs and register variants among them. A language has a case when some word distinguishes it by form, and the other words may realize it with the form of another case ([Cor08]), so a fragment with paradigms proves that they separate its cases. The hierarchies and orders the literature places on the comparative values are each stated where they are used: the containment orders in Syntax/Case/Order.lean and Blake's hierarchy of case systems in Studies/Blake1994.lean.

The Universal Dependencies case tags are the corpus vocabulary, reached through Morphology/Word/UD.lean ([dMMNZ21]). Every value realizes as a tag and every tag ingests as a value. The oblique realizes as Acc, the tag UD's guidelines give the oblique of a language with only a direct and an oblique case, and so ingests back as the accusative.

Main declarations

• Case: the comparative case values.

References

• [Bla94b]
• [Bla01]
• [Cor08]
• [Has10]
• [dMMNZ21]

inductive Case : Type

Grammatical case — the canonical analytical inventory.

• nom : Case

  Nominative: citation/subject case.

• acc : Case

  Accusative: direct object.

• gen : Case

  Genitive: possessor, nominal dependent.

• dat : Case

  Dative: indirect object, recipient.

• inst : Case

  Instrumental: means, instrument.

• loc : Case

  Locative: static location (general).

• voc : Case

  Vocative: address form.

• abl : Case

  Ablative: source, motion from (general).

• erg : Case

  Ergative: transitive subject in ergative alignment.

• abs : Case

  Absolutive: intransitive subject / transitive object in ergative alignment.

• obl : Case

  Oblique: the non-nominative case of a system of direct and oblique cases, the form the adpositions govern, Blake's label for a second case of many functions ([Bla01] p. 156).

• part : Case

  Partitive: partial affectedness, indeterminate quantity (Finnic).

• ess : Case

  Essive: temporary state, capacity ("as an X").

• transl : Case

  Translative: change of state ("into an X").

• com : Case

  Comitative: accompaniment ("with X").

• ade : Case

  Adessive: at/near (exterior static).

• ine : Case

  Inessive: in (interior static).

• ill : Case

  Illative: into (interior goal).

• ela : Case

  Elative: out of (interior source).

• all : Case

  Allative: onto/towards (exterior goal).

• sub : Case

  Sublative: onto (surface goal; Hungarian).

• sup : Case

  Superessive: on (surface static; Hungarian).

• del : Case

  Delative: off of (surface source; Hungarian).

• ter : Case

  Terminative: up to a limit ("as far as X").

• tem : Case

  Temporal: at a time.

• caus : Case

  Causative/causal: because of X.

• ben : Case

  Benefactive: for the benefit of X.

• perl : Case

  Perlative: path, motion through.

• abess : Case

  Abessive/privative: without X.

@[instance_reducible]

instance instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance instReprCase : Repr Case

Equations

• instReprCase = { reprPrec := instReprCase.repr }

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

Equations

• instReprCase.repr Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.nom")).group prec✝
• instReprCase.repr Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.acc")).group prec✝
• instReprCase.repr Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.gen")).group prec✝
• instReprCase.repr Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.dat")).group prec✝
• instReprCase.repr Case.inst prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.inst")).group prec✝
• instReprCase.repr Case.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.loc")).group prec✝
• instReprCase.repr Case.voc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.voc")).group prec✝
• instReprCase.repr Case.abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.abl")).group prec✝
• instReprCase.repr Case.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.erg")).group prec✝
• instReprCase.repr Case.abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.abs")).group prec✝
• instReprCase.repr Case.obl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.obl")).group prec✝
• instReprCase.repr Case.part prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.part")).group prec✝
• instReprCase.repr Case.ess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ess")).group prec✝
• instReprCase.repr Case.transl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.transl")).group prec✝
• instReprCase.repr Case.com prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.com")).group prec✝
• instReprCase.repr Case.ade prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ade")).group prec✝
• instReprCase.repr Case.ine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ine")).group prec✝
• instReprCase.repr Case.ill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ill")).group prec✝
• instReprCase.repr Case.ela prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ela")).group prec✝
• instReprCase.repr Case.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.all")).group prec✝
• instReprCase.repr Case.sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.sub")).group prec✝
• instReprCase.repr Case.sup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.sup")).group prec✝
• instReprCase.repr Case.del prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.del")).group prec✝
• instReprCase.repr Case.ter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ter")).group prec✝
• instReprCase.repr Case.tem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.tem")).group prec✝
• instReprCase.repr Case.caus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.caus")).group prec✝
• instReprCase.repr Case.ben prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.ben")).group prec✝
• instReprCase.repr Case.perl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.perl")).group prec✝
• instReprCase.repr Case.abess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.abess")).group prec✝

@[instance_reducible]

instance instInhabitedCase : Inhabited Case

Equations

• instInhabitedCase = { default := instInhabitedCase.default }

@[instance_reducible]

instance instFintypeCase : Fintype Case

Equations

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