Case — Basic Definitions

@cite{de-marneffe-zeman-2021} @cite{blake-1994} @cite{stassen-1985}

The Core.Case type itself (a definitional alias for UD.Case), the lowercase constructor abbrevs that mirror the UD PascalCase ones, and the small enums for alignment family and case assignment.

Both naming conventions are valid: .Nom/.Acc (UD PascalCase) and .nom/.acc (theoretical lowercase) refer to the same constructors, via @[match_pattern] abbrevs in Core/Lexical/UD.lean and here.

inductive Core.AlignmentFamily : Type

The two major morphosyntactic alignment families.

• accusative : AlignmentFamily
• ergative : AlignmentFamily

@[implicit_reducible]

instance Core.instDecidableEqAlignmentFamily : DecidableEq AlignmentFamily

Equations

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

@[implicit_reducible]

instance Core.instReprAlignmentFamily : Repr AlignmentFamily

Equations

• Core.instReprAlignmentFamily = { reprPrec := Core.instReprAlignmentFamily.repr }

def Core.instReprAlignmentFamily.repr : AlignmentFamily → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Core.Case : Type

Cross-linguistic case inventory. Definitional alias for UD.Case — the Universal Dependencies treebank tagset (28 constructors). All theoretical machinery (Blake hierarchy, Anderson features, Caha containment, Heine grammaticalization) operates over this same type, ensuring there is a single source of truth shared between UD-annotated lexical data and theoretical analyses.

Equations

• Core.Case = UD.Case

@[implicit_reducible]

instance Core.instFintypeCase : Fintype Case

Equations

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

Lowercase match_pattern constructor aliases (.nom, .acc, …) live in the canonical UD.Case namespace (Core/Lexical/UD.lean). Since Core.Case = UD.Case, dot-notation (.nom : Core.Case) resolves through that single source of truth — no separate Core.Case.* aliases are needed.

theorem Core.Case.card_univ : Finset.univ.card = 28

The 28 UD case constructors are exhaustive.

inductive Core.CaseAssignment : Type

How case is assigned to an NP in a given construction (@cite{stassen-1985}, §2.2.1).

• derived : CaseAssignment
• fixed : CaseAssignment

@[implicit_reducible]

instance Core.instDecidableEqCaseAssignment : DecidableEq CaseAssignment

Equations

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

@[implicit_reducible]

instance Core.instReprCaseAssignment : Repr CaseAssignment

Equations

• Core.instReprCaseAssignment = { reprPrec := Core.instReprCaseAssignment.repr }

def Core.instReprCaseAssignment.repr : CaseAssignment → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.instReprCaseAssignment.repr Core.CaseAssignment.fixed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.CaseAssignment.fixed")).group prec✝

inductive Core.FixedCaseEncoding : Type

For fixed-case NPs, what syntactic role the NP occupies.

• directObject : FixedCaseEncoding
• adverbial : FixedCaseEncoding

@[implicit_reducible]

instance Core.instDecidableEqFixedCaseEncoding : DecidableEq FixedCaseEncoding

Equations

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

@[implicit_reducible]

instance Core.instReprFixedCaseEncoding : Repr FixedCaseEncoding

Equations

• Core.instReprFixedCaseEncoding = { reprPrec := Core.instReprFixedCaseEncoding.repr }

def Core.instReprFixedCaseEncoding.repr : FixedCaseEncoding → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.