Universal Dependencies Types

[dMMNZ21]

Universal part-of-speech tags (UPOS), morphological features, and dependency relations from UD v2.

These provide theory-neutral lexical categories, morphological annotations, and grammatical relations that can be used throughout the library and mapped to/from theory-specific categories (CCG.Cat, Minimalism features, DG trees, etc.).

Official site: https://universaldependencies.org/

Provenance

UD is an external annotation standard ([dMMNZ21]); this file is the linglib mirror of its v2 surface, and Data/UD/ is the standard's area — treebank data (CoNLL-U) belongs here beside the vocabulary, paralleling Data/WALS/ (schema + datapoints). Its types are the foundational substrate every other layer builds on: Features/ aliases the feature types (e.g. Number.fromUD/Number.toUD, …) and Morphology/Word.lean builds the ms-word token over the vocabulary. The bare UD namespace (no Data. prefix) is intentional — UD is its own external project. Subsumption-order theory over MorphFeatures lives in Morphology/Unification.lean (mathlib-importing); this file stays mathlib-light.

inductive UD.UPOS : Type

Universal part-of-speech tags (UPOS).

17 coarse-grained categories designed for cross-linguistic consistency. Every word in every language can be assigned one of these tags.

• ADJ : UPOS
• ADV : UPOS
• INTJ : UPOS
• NOUN : UPOS
• PROPN : UPOS
• VERB : UPOS
• ADP : UPOS
• AUX : UPOS
• CCONJ : UPOS
• DET : UPOS
• NUM : UPOS
• PART : UPOS
• PRON : UPOS
• SCONJ : UPOS
• PUNCT : UPOS
• SYM : UPOS
• X : UPOS

@[implicit_reducible]

instance UD.instDecidableEqUPOS : DecidableEq UPOS

Equations

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

def UD.instReprUPOS.repr : UPOS → ℕ → Std.Format

Equations

• UD.instReprUPOS.repr UD.UPOS.ADJ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.ADJ")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.ADV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.ADV")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.INTJ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.INTJ")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.NOUN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.NOUN")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.PROPN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.PROPN")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.VERB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.VERB")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.ADP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.ADP")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.AUX prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.AUX")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.CCONJ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.CCONJ")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.DET prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.DET")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.NUM prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.NUM")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.PART prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.PART")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.PRON prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.PRON")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.SCONJ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.SCONJ")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.PUNCT prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.PUNCT")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.SYM prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.SYM")).group prec✝
• UD.instReprUPOS.repr UD.UPOS.X prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.UPOS.X")).group prec✝

@[implicit_reducible]

instance UD.instReprUPOS : Repr UPOS

Equations

• UD.instReprUPOS = { reprPrec := UD.instReprUPOS.repr }

@[implicit_reducible]

instance UD.instInhabitedUPOS : Inhabited UPOS

Equations

• UD.instInhabitedUPOS = { default := UD.instInhabitedUPOS.default }

def UD.instHashableUPOS.hash : UPOS → UInt64

Equations

• UD.instHashableUPOS.hash UD.UPOS.ADJ = 0
• UD.instHashableUPOS.hash UD.UPOS.ADV = 1
• UD.instHashableUPOS.hash UD.UPOS.INTJ = 2
• UD.instHashableUPOS.hash UD.UPOS.NOUN = 3
• UD.instHashableUPOS.hash UD.UPOS.PROPN = 4
• UD.instHashableUPOS.hash UD.UPOS.VERB = 5
• UD.instHashableUPOS.hash UD.UPOS.ADP = 6
• UD.instHashableUPOS.hash UD.UPOS.AUX = 7
• UD.instHashableUPOS.hash UD.UPOS.CCONJ = 8
• UD.instHashableUPOS.hash UD.UPOS.DET = 9
• UD.instHashableUPOS.hash UD.UPOS.NUM = 10
• UD.instHashableUPOS.hash UD.UPOS.PART = 11
• UD.instHashableUPOS.hash UD.UPOS.PRON = 12
• UD.instHashableUPOS.hash UD.UPOS.SCONJ = 13
• UD.instHashableUPOS.hash UD.UPOS.PUNCT = 14
• UD.instHashableUPOS.hash UD.UPOS.SYM = 15
• UD.instHashableUPOS.hash UD.UPOS.X = 16

@[implicit_reducible]

instance UD.instHashableUPOS : Hashable UPOS

Equations

• UD.instHashableUPOS = { hash := UD.instHashableUPOS.hash }

def UD.UPOS.toString : UPOS → String

String representation matching UD conventions

Equations

• UD.UPOS.ADJ.toString = "ADJ"
• UD.UPOS.ADV.toString = "ADV"
• UD.UPOS.INTJ.toString = "INTJ"
• UD.UPOS.NOUN.toString = "NOUN"
• UD.UPOS.PROPN.toString = "PROPN"
• UD.UPOS.VERB.toString = "VERB"
• UD.UPOS.ADP.toString = "ADP"
• UD.UPOS.AUX.toString = "AUX"
• UD.UPOS.CCONJ.toString = "CCONJ"
• UD.UPOS.DET.toString = "DET"
• UD.UPOS.NUM.toString = "NUM"
• UD.UPOS.PART.toString = "PART"
• UD.UPOS.PRON.toString = "PRON"
• UD.UPOS.SCONJ.toString = "SCONJ"
• UD.UPOS.PUNCT.toString = "PUNCT"
• UD.UPOS.SYM.toString = "SYM"
• UD.UPOS.X.toString = "X"

@[implicit_reducible]

instance UD.instToStringUPOS : ToString UPOS

Equations

• UD.instToStringUPOS = { toString := UD.UPOS.toString }

def UD.UPOS.isOpenClass : UPOS → Bool

Is this an open class (content) word?

Equations

• UD.UPOS.ADJ.isOpenClass = true
• UD.UPOS.ADV.isOpenClass = true
• UD.UPOS.INTJ.isOpenClass = true
• UD.UPOS.NOUN.isOpenClass = true
• UD.UPOS.PROPN.isOpenClass = true
• UD.UPOS.VERB.isOpenClass = true
• x✝.isOpenClass = false

def UD.UPOS.isClosedClass : UPOS → Bool

Is this a closed class (function) word?

Equations

• UD.UPOS.ADP.isClosedClass = true
• UD.UPOS.AUX.isClosedClass = true
• UD.UPOS.CCONJ.isClosedClass = true
• UD.UPOS.DET.isClosedClass = true
• UD.UPOS.NUM.isClosedClass = true
• UD.UPOS.PART.isClosedClass = true
• UD.UPOS.PRON.isClosedClass = true
• UD.UPOS.SCONJ.isClosedClass = true
• x✝.isClosedClass = false

def UD.UPOS.isNominal : UPOS → Bool

Is this a nominal (entity-denoting) category?

Equations

• UD.UPOS.NOUN.isNominal = true
• UD.UPOS.PROPN.isNominal = true
• UD.UPOS.PRON.isNominal = true
• UD.UPOS.NUM.isNominal = true
• x✝.isNominal = false

def UD.UPOS.isPredicate : UPOS → Bool

Is this a predicate (event-denoting) category?

Equations

• UD.UPOS.VERB.isPredicate = true
• UD.UPOS.AUX.isPredicate = true
• x✝.isPredicate = false

def UD.UPOS.isModifier : UPOS → Bool

Is this a modifier category?

Equations

• UD.UPOS.ADJ.isModifier = true
• UD.UPOS.ADV.isModifier = true
• x✝.isModifier = false

inductive UD.Number : Type

Grammatical number

• Sing : Number
• Plur : Number
• Dual : Number
• Tri : Number
• Pauc : Number
• Grpa : Number
• Grpl : Number
• Inv : Number
• Coll : Number
• Count : Number

@[implicit_reducible]

instance UD.instDecidableEqNumber : DecidableEq Number

Equations

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

@[implicit_reducible]

instance UD.instReprNumber : Repr Number

Equations

• UD.instReprNumber = { reprPrec := UD.instReprNumber.repr }

def UD.instReprNumber.repr : Number → ℕ → Std.Format

Equations

• UD.instReprNumber.repr UD.Number.Sing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Sing")).group prec✝
• UD.instReprNumber.repr UD.Number.Plur prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Plur")).group prec✝
• UD.instReprNumber.repr UD.Number.Dual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Dual")).group prec✝
• UD.instReprNumber.repr UD.Number.Tri prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Tri")).group prec✝
• UD.instReprNumber.repr UD.Number.Pauc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Pauc")).group prec✝
• UD.instReprNumber.repr UD.Number.Grpa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Grpa")).group prec✝
• UD.instReprNumber.repr UD.Number.Grpl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Grpl")).group prec✝
• UD.instReprNumber.repr UD.Number.Inv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Inv")).group prec✝
• UD.instReprNumber.repr UD.Number.Coll prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Coll")).group prec✝
• UD.instReprNumber.repr UD.Number.Count prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Number.Count")).group prec✝

@[implicit_reducible]

instance UD.instInhabitedNumber : Inhabited Number

Equations

• UD.instInhabitedNumber = { default := UD.instInhabitedNumber.default }

inductive UD.Gender : Type

Grammatical gender

• Masc : Gender
• Fem : Gender
• Neut : Gender
• Com : Gender

@[implicit_reducible]

instance UD.instDecidableEqGender : DecidableEq Gender

Equations

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

def UD.instReprGender.repr : Gender → ℕ → Std.Format

Equations

• UD.instReprGender.repr UD.Gender.Masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Gender.Masc")).group prec✝
• UD.instReprGender.repr UD.Gender.Fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Gender.Fem")).group prec✝
• UD.instReprGender.repr UD.Gender.Neut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Gender.Neut")).group prec✝
• UD.instReprGender.repr UD.Gender.Com prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Gender.Com")).group prec✝

@[implicit_reducible]

instance UD.instReprGender : Repr Gender

Equations

• UD.instReprGender = { reprPrec := UD.instReprGender.repr }

@[implicit_reducible]

instance UD.instInhabitedGender : Inhabited Gender

Equations

• UD.instInhabitedGender = { default := UD.instInhabitedGender.default }

inductive UD.Case : Type

Grammatical case (UD Case feature, https://universaldependencies.org/u/feat/Case.html).

Battle-tested annotation tagset shared across all UD treebanks. The 28 constructors below cover the standard UD values. This is the realization vocabulary; the canonical analytical inventory is the root-namespace Case (Features/Case/Basic.lean), reachable by Case.toUD/Case.fromUD.

• Nom : Case
• Acc : Case
• Gen : Case
• Dat : Case
• Ins : Case
• Loc : Case
• Voc : Case
• Abl : Case
• Erg : Case
• Abs : Case
• Par : Case
• Ess : Case
• Tra : Case
• Com : Case
• Ade : Case
• Ine : Case
• Ill : Case
• Ela : Case
• All : Case
• Sub : Case
• Sup : Case
• Del : Case
• Ter : Case
• Tem : Case
• Cau : Case
• Ben : Case
• Per : Case
• Abe : Case

@[implicit_reducible]

instance UD.instDecidableEqCase : DecidableEq Case

Equations

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

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

Equations

• UD.instReprCase.repr UD.Case.Nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Nom")).group prec✝
• UD.instReprCase.repr UD.Case.Acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Acc")).group prec✝
• UD.instReprCase.repr UD.Case.Gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Gen")).group prec✝
• UD.instReprCase.repr UD.Case.Dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Dat")).group prec✝
• UD.instReprCase.repr UD.Case.Ins prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Ins")).group prec✝
• UD.instReprCase.repr UD.Case.Loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Loc")).group prec✝
• UD.instReprCase.repr UD.Case.Voc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Voc")).group prec✝
• UD.instReprCase.repr UD.Case.Abl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Abl")).group prec✝
• UD.instReprCase.repr UD.Case.Erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Erg")).group prec✝
• UD.instReprCase.repr UD.Case.Abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Abs")).group prec✝
• UD.instReprCase.repr UD.Case.Par prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Par")).group prec✝
• UD.instReprCase.repr UD.Case.Ess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Ess")).group prec✝
• UD.instReprCase.repr UD.Case.Tra prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Tra")).group prec✝
• UD.instReprCase.repr UD.Case.Com prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Com")).group prec✝
• UD.instReprCase.repr UD.Case.Ade prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Ade")).group prec✝
• UD.instReprCase.repr UD.Case.Ine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Ine")).group prec✝
• UD.instReprCase.repr UD.Case.Ill prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Ill")).group prec✝
• UD.instReprCase.repr UD.Case.Ela prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Ela")).group prec✝
• UD.instReprCase.repr UD.Case.All prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.All")).group prec✝
• UD.instReprCase.repr UD.Case.Sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Sub")).group prec✝
• UD.instReprCase.repr UD.Case.Sup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Sup")).group prec✝
• UD.instReprCase.repr UD.Case.Del prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Del")).group prec✝
• UD.instReprCase.repr UD.Case.Ter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Ter")).group prec✝
• UD.instReprCase.repr UD.Case.Tem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Tem")).group prec✝
• UD.instReprCase.repr UD.Case.Cau prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Cau")).group prec✝
• UD.instReprCase.repr UD.Case.Ben prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Ben")).group prec✝
• UD.instReprCase.repr UD.Case.Per prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Per")).group prec✝
• UD.instReprCase.repr UD.Case.Abe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Case.Abe")).group prec✝

@[implicit_reducible]

instance UD.instReprCase : Repr Case

Equations

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

@[implicit_reducible]

instance UD.instInhabitedCase : Inhabited Case

Equations

• UD.instInhabitedCase = { default := UD.instInhabitedCase.default }

@[implicit_reducible]

instance UD.instFintypeCase : Fintype Case

Equations

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

inductive UD.Definite : Type

Definiteness

• Def : Definite
• Ind : Definite
• Spec : Definite
• Cons : Definite

@[implicit_reducible]

instance UD.instDecidableEqDefinite : DecidableEq Definite

Equations

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

@[implicit_reducible]

instance UD.instReprDefinite : Repr Definite

Equations

• UD.instReprDefinite = { reprPrec := UD.instReprDefinite.repr }

def UD.instReprDefinite.repr : Definite → ℕ → Std.Format

Equations

• UD.instReprDefinite.repr UD.Definite.Def prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Definite.Def")).group prec✝
• UD.instReprDefinite.repr UD.Definite.Ind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Definite.Ind")).group prec✝
• UD.instReprDefinite.repr UD.Definite.Spec prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Definite.Spec")).group prec✝
• UD.instReprDefinite.repr UD.Definite.Cons prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Definite.Cons")).group prec✝

@[implicit_reducible]

instance UD.instInhabitedDefinite : Inhabited Definite

Equations

• UD.instInhabitedDefinite = { default := UD.instInhabitedDefinite.default }

inductive UD.Degree : Type

Degree of comparison (for adjectives/adverbs)

• Pos : Degree
• Cmp : Degree
• Sup : Degree
• Abs : Degree
• Equ : Degree

@[implicit_reducible]

instance UD.instDecidableEqDegree : DecidableEq Degree

Equations

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

def UD.instReprDegree.repr : Degree → ℕ → Std.Format

Equations

• UD.instReprDegree.repr UD.Degree.Pos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Degree.Pos")).group prec✝
• UD.instReprDegree.repr UD.Degree.Cmp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Degree.Cmp")).group prec✝
• UD.instReprDegree.repr UD.Degree.Sup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Degree.Sup")).group prec✝
• UD.instReprDegree.repr UD.Degree.Abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Degree.Abs")).group prec✝
• UD.instReprDegree.repr UD.Degree.Equ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Degree.Equ")).group prec✝

@[implicit_reducible]

instance UD.instReprDegree : Repr Degree

Equations

• UD.instReprDegree = { reprPrec := UD.instReprDegree.repr }

@[implicit_reducible]

instance UD.instInhabitedDegree : Inhabited Degree

Equations

• UD.instInhabitedDegree = { default := UD.instInhabitedDegree.default }

inductive UD.PronType : Type

Pronoun type

• Prs : PronType
• Rcp : PronType
• Art : PronType
• Int : PronType
• Rel : PronType
• Dem : PronType
• Emp : PronType
• Tot : PronType
• Neg : PronType
• Ind : PronType
• Exc : PronType

@[implicit_reducible]

instance UD.instDecidableEqPronType : DecidableEq PronType

Equations

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

@[implicit_reducible]

instance UD.instReprPronType : Repr PronType

Equations

• UD.instReprPronType = { reprPrec := UD.instReprPronType.repr }

def UD.instReprPronType.repr : PronType → ℕ → Std.Format

Equations

• UD.instReprPronType.repr UD.PronType.Prs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Prs")).group prec✝
• UD.instReprPronType.repr UD.PronType.Rcp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Rcp")).group prec✝
• UD.instReprPronType.repr UD.PronType.Art prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Art")).group prec✝
• UD.instReprPronType.repr UD.PronType.Int prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Int")).group prec✝
• UD.instReprPronType.repr UD.PronType.Rel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Rel")).group prec✝
• UD.instReprPronType.repr UD.PronType.Dem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Dem")).group prec✝
• UD.instReprPronType.repr UD.PronType.Emp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Emp")).group prec✝
• UD.instReprPronType.repr UD.PronType.Tot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Tot")).group prec✝
• UD.instReprPronType.repr UD.PronType.Neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Neg")).group prec✝
• UD.instReprPronType.repr UD.PronType.Ind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Ind")).group prec✝
• UD.instReprPronType.repr UD.PronType.Exc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.PronType.Exc")).group prec✝

@[implicit_reducible]

instance UD.instInhabitedPronType : Inhabited PronType

Equations

• UD.instInhabitedPronType = { default := UD.instInhabitedPronType.default }

inductive UD.Person : Type

Grammatical person

• first : Person
• second : Person
• third : Person
• zero : Person

@[implicit_reducible]

instance UD.instDecidableEqPerson : DecidableEq Person

Equations

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

@[implicit_reducible]

instance UD.instReprPerson : Repr Person

Equations

• UD.instReprPerson = { reprPrec := UD.instReprPerson.repr }

def UD.instReprPerson.repr : Person → ℕ → Std.Format

Equations

• UD.instReprPerson.repr UD.Person.first prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Person.first")).group prec✝
• UD.instReprPerson.repr UD.Person.second prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Person.second")).group prec✝
• UD.instReprPerson.repr UD.Person.third prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Person.third")).group prec✝
• UD.instReprPerson.repr UD.Person.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Person.zero")).group prec✝

@[implicit_reducible]

instance UD.instInhabitedPerson : Inhabited Person

Equations

• UD.instInhabitedPerson = { default := UD.instInhabitedPerson.default }

inductive UD.VerbForm : Type

Verb form

• Fin : VerbForm
• Inf : VerbForm
• Part : VerbForm
• Ger : VerbForm
• Gdv : VerbForm
• Sup : VerbForm
• Conv : VerbForm
• Vnoun : VerbForm

@[implicit_reducible]

instance UD.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

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

def UD.instReprVerbForm.repr : VerbForm → ℕ → Std.Format

Equations

• UD.instReprVerbForm.repr UD.VerbForm.Fin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.VerbForm.Fin")).group prec✝
• UD.instReprVerbForm.repr UD.VerbForm.Inf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.VerbForm.Inf")).group prec✝
• UD.instReprVerbForm.repr UD.VerbForm.Part prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.VerbForm.Part")).group prec✝
• UD.instReprVerbForm.repr UD.VerbForm.Ger prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.VerbForm.Ger")).group prec✝
• UD.instReprVerbForm.repr UD.VerbForm.Gdv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.VerbForm.Gdv")).group prec✝
• UD.instReprVerbForm.repr UD.VerbForm.Sup prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.VerbForm.Sup")).group prec✝
• UD.instReprVerbForm.repr UD.VerbForm.Conv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.VerbForm.Conv")).group prec✝
• UD.instReprVerbForm.repr UD.VerbForm.Vnoun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.VerbForm.Vnoun")).group prec✝

@[implicit_reducible]

instance UD.instReprVerbForm : Repr VerbForm

Equations

• UD.instReprVerbForm = { reprPrec := UD.instReprVerbForm.repr }

@[implicit_reducible]

instance UD.instInhabitedVerbForm : Inhabited VerbForm

Equations

• UD.instInhabitedVerbForm = { default := UD.instInhabitedVerbForm.default }

inductive UD.Tense : Type

Grammatical tense

• Past : Tense
• Pres : Tense
• Fut : Tense
• Imp : Tense
• Pqp : Tense

@[implicit_reducible]

instance UD.instDecidableEqTense : DecidableEq Tense

Equations

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

def UD.instReprTense.repr : Tense → ℕ → Std.Format

Equations

• UD.instReprTense.repr UD.Tense.Past prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Tense.Past")).group prec✝
• UD.instReprTense.repr UD.Tense.Pres prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Tense.Pres")).group prec✝
• UD.instReprTense.repr UD.Tense.Fut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Tense.Fut")).group prec✝
• UD.instReprTense.repr UD.Tense.Imp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Tense.Imp")).group prec✝
• UD.instReprTense.repr UD.Tense.Pqp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Tense.Pqp")).group prec✝

@[implicit_reducible]

instance UD.instReprTense : Repr Tense

Equations

• UD.instReprTense = { reprPrec := UD.instReprTense.repr }

@[implicit_reducible]

instance UD.instInhabitedTense : Inhabited Tense

Equations

• UD.instInhabitedTense = { default := UD.instInhabitedTense.default }

inductive UD.Aspect : Type

Grammatical aspect

• Imp : Aspect
• Perf : Aspect
• Prog : Aspect
• Prosp : Aspect
• Hab : Aspect
• Iter : Aspect

@[implicit_reducible]

instance UD.instDecidableEqAspect : DecidableEq Aspect

Equations

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

@[implicit_reducible]

instance UD.instReprAspect : Repr Aspect

Equations

• UD.instReprAspect = { reprPrec := UD.instReprAspect.repr }

def UD.instReprAspect.repr : Aspect → ℕ → Std.Format

Equations

• UD.instReprAspect.repr UD.Aspect.Imp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Aspect.Imp")).group prec✝
• UD.instReprAspect.repr UD.Aspect.Perf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Aspect.Perf")).group prec✝
• UD.instReprAspect.repr UD.Aspect.Prog prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Aspect.Prog")).group prec✝
• UD.instReprAspect.repr UD.Aspect.Prosp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Aspect.Prosp")).group prec✝
• UD.instReprAspect.repr UD.Aspect.Hab prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Aspect.Hab")).group prec✝
• UD.instReprAspect.repr UD.Aspect.Iter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Aspect.Iter")).group prec✝

@[implicit_reducible]

instance UD.instInhabitedAspect : Inhabited Aspect

Equations

• UD.instInhabitedAspect = { default := UD.instInhabitedAspect.default }

inductive UD.Mood : Type

Grammatical mood

• Ind : Mood
• Sub : Mood
• Imp : Mood
• Cnd : Mood
• Opt : Mood
• Jus : Mood
• Pot : Mood
• Qot : Mood
• Adm : Mood
• Nec : Mood
• Irr : Mood

@[implicit_reducible]

instance UD.instDecidableEqMood : DecidableEq Mood

Equations

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

@[implicit_reducible]

instance UD.instReprMood : Repr Mood

Equations

• UD.instReprMood = { reprPrec := UD.instReprMood.repr }

def UD.instReprMood.repr : Mood → ℕ → Std.Format

Equations

• UD.instReprMood.repr UD.Mood.Ind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Ind")).group prec✝
• UD.instReprMood.repr UD.Mood.Sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Sub")).group prec✝
• UD.instReprMood.repr UD.Mood.Imp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Imp")).group prec✝
• UD.instReprMood.repr UD.Mood.Cnd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Cnd")).group prec✝
• UD.instReprMood.repr UD.Mood.Opt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Opt")).group prec✝
• UD.instReprMood.repr UD.Mood.Jus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Jus")).group prec✝
• UD.instReprMood.repr UD.Mood.Pot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Pot")).group prec✝
• UD.instReprMood.repr UD.Mood.Qot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Qot")).group prec✝
• UD.instReprMood.repr UD.Mood.Adm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Adm")).group prec✝
• UD.instReprMood.repr UD.Mood.Nec prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Nec")).group prec✝
• UD.instReprMood.repr UD.Mood.Irr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Mood.Irr")).group prec✝

@[implicit_reducible]

instance UD.instInhabitedMood : Inhabited Mood

Equations

• UD.instInhabitedMood = { default := UD.instInhabitedMood.default }

inductive UD.Voice : Type

Grammatical voice

• Act : Voice
• Pass : Voice
• Mid : Voice
• Rcp : Voice
• Cau : Voice
• Antip : Voice
• Dir : Voice
• Inv : Voice
• Lfoc : Voice
• Bfoc : Voice

@[implicit_reducible]

instance UD.instDecidableEqVoice : DecidableEq Voice

Equations

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

def UD.instReprVoice.repr : Voice → ℕ → Std.Format

Equations

• UD.instReprVoice.repr UD.Voice.Act prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Act")).group prec✝
• UD.instReprVoice.repr UD.Voice.Pass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Pass")).group prec✝
• UD.instReprVoice.repr UD.Voice.Mid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Mid")).group prec✝
• UD.instReprVoice.repr UD.Voice.Rcp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Rcp")).group prec✝
• UD.instReprVoice.repr UD.Voice.Cau prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Cau")).group prec✝
• UD.instReprVoice.repr UD.Voice.Antip prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Antip")).group prec✝
• UD.instReprVoice.repr UD.Voice.Dir prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Dir")).group prec✝
• UD.instReprVoice.repr UD.Voice.Inv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Inv")).group prec✝
• UD.instReprVoice.repr UD.Voice.Lfoc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Lfoc")).group prec✝
• UD.instReprVoice.repr UD.Voice.Bfoc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Voice.Bfoc")).group prec✝

@[implicit_reducible]

instance UD.instReprVoice : Repr Voice

Equations

• UD.instReprVoice = { reprPrec := UD.instReprVoice.repr }

@[implicit_reducible]

instance UD.instInhabitedVoice : Inhabited Voice

Equations

• UD.instInhabitedVoice = { default := UD.instInhabitedVoice.default }

inductive UD.Polarity : Type

Polarity

• Pos : Polarity
• Neg : Polarity

@[implicit_reducible]

instance UD.instDecidableEqPolarity : DecidableEq Polarity

Equations

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

@[implicit_reducible]

instance UD.instReprPolarity : Repr Polarity

Equations

• UD.instReprPolarity = { reprPrec := UD.instReprPolarity.repr }

def UD.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

• UD.instReprPolarity.repr UD.Polarity.Pos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Polarity.Pos")).group prec✝
• UD.instReprPolarity.repr UD.Polarity.Neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.Polarity.Neg")).group prec✝

@[implicit_reducible]

instance UD.instInhabitedPolarity : Inhabited Polarity

Equations

• UD.instInhabitedPolarity = { default := UD.instInhabitedPolarity.default }

structure UD.MorphFeatures : Type

A morphological feature bundle (partial assignment). Uses Option to represent unspecified features.

• number : Option Number
• gender : Option Gender
• case_ : Option Case
• definite : Option Definite
• degree : Option Degree
• pronType : Option PronType
• reflex : Bool

  Reflexive (UD Reflex=Yes); false = feature absent. Distinguishes a reflexive anaphor from a plain personal pronoun; not an agreement feature, so not consulted by compatible.

• person : Option Person
• verbForm : Option VerbForm
• tense : Option Tense
• aspect : Option Aspect
• mood : Option Mood
• voice : Option Voice
• polarity : Option Polarity

def UD.instDecidableEqMorphFeatures.decEq (x✝ x✝¹ : MorphFeatures) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance UD.instDecidableEqMorphFeatures : DecidableEq MorphFeatures

Equations

• UD.instDecidableEqMorphFeatures = UD.instDecidableEqMorphFeatures.decEq

def UD.instReprMorphFeatures.repr : MorphFeatures → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance UD.instReprMorphFeatures : Repr MorphFeatures

Equations

• UD.instReprMorphFeatures = { reprPrec := UD.instReprMorphFeatures.repr }

@[implicit_reducible]

instance UD.instInhabitedMorphFeatures : Inhabited MorphFeatures

Equations

• UD.instInhabitedMorphFeatures = { default := UD.instInhabitedMorphFeatures.default }

def UD.MorphFeatures.empty : MorphFeatures

Empty feature bundle

Equations

• UD.MorphFeatures.empty = { }

def UD.MorphFeatures.isWh (f : MorphFeatures) : Bool

Is this bundle wh-marked — an interrogative or relative pro-form? Derived from pronType (UD has no standalone wh feature; wh-ness is PronType ∈ {Int, Rel}).

Equations

• f.isWh = (f.pronType == some UD.PronType.Int || f.pronType == some UD.PronType.Rel)

def UD.MorphFeatures.compatible (f1 f2 : MorphFeatures) : Bool

Are two feature bundles compatible — bounded above in the subsumption order ([Shi86] §3.2.3)? Total over all option-valued fields: a conflict in any committed feature makes unification fail. (reflex needs no clause — a Bool slot with false = absent is always joinable by ||.) The order-theoretic characterization is proved in Morphology/Unification.lean.

Equations

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

@[simp]

theorem UD.MorphFeatures.compatible_self (f : MorphFeatures) : f.compatible f = true

Feature compatibility is reflexive: every bundle is compatible with itself (each feature matches itself).

theorem UD.MorphFeatures.compatible_comm (f1 f2 : MorphFeatures) : f1.compatible f2 = f2.compatible f1

Feature compatibility is symmetric.

Per-slot projections of compatible

φ-compatibility is a conjunction over all slots; these project it onto a single slot's clause. They confine the coupling to compatible's clause layout to this one site, beside the definition, so the per-feature faithfulness theorems (HasX.compatible_hasX in Features/{Person,Number,Gender,Case}/Capabilities.lean) consume a named edge rather than each re-unfolding the definition. Only the four φ-slots that carry a HasX mixin are projected.

theorem UD.MorphFeatures.compatible_number {f1 f2 : MorphFeatures} (h : f1.compatible f2 = true) : (f1.number.isNone || f2.number.isNone || f1.number == f2.number) = true

Project φ-compatibility onto its number clause.

theorem UD.MorphFeatures.compatible_gender {f1 f2 : MorphFeatures} (h : f1.compatible f2 = true) : (f1.gender.isNone || f2.gender.isNone || f1.gender == f2.gender) = true

Project φ-compatibility onto its gender clause.

theorem UD.MorphFeatures.compatible_case {f1 f2 : MorphFeatures} (h : f1.compatible f2 = true) : (f1.case_.isNone || f2.case_.isNone || f1.case_ == f2.case_) = true

Project φ-compatibility onto its case clause.

theorem UD.MorphFeatures.compatible_person {f1 f2 : MorphFeatures} (h : f1.compatible f2 = true) : (f1.person.isNone || f2.person.isNone || f1.person == f2.person) = true

Project φ-compatibility onto its person clause.

def UD.MorphFeatures.merge (f1 f2 : MorphFeatures) : MorphFeatures

The information-join of two bundles, field-by-field: keep every committed value (left-biased per field, which on compatible inputs is symmetric since doubly committed fields agree). Only meaningful under compatible; unify adds the guard.

Equations

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

def UD.MorphFeatures.unify (f1 f2 : MorphFeatures) : Option MorphFeatures

Unify two feature bundles ([Shi86] §3.2.3): the least upper bound in the subsumption order when the bundles are compatible (Morphology/Unification.lean proves the lub laws), failure (none) on conflicting information.

Equations

• f1.unify f2 = if f1.compatible f2 = true then some (f1.merge f2) else none

inductive UD.DepRel : Type

Universal dependency relations.

Organized by function following the UD documentation. These encode grammatical relations between a head and its dependent.

Reference: https://universaldependencies.org/u/dep/

• nsubj : DepRel
• nsubjPass : DepRel
• csubj : DepRel
• csubjPass : DepRel
• obj : DepRel
• iobj : DepRel
• ccomp : DepRel
• xcomp : DepRel
• obl : DepRel
• vocative : DepRel
• expl : DepRel
• dislocated : DepRel
• advcl : DepRel
• nmod : DepRel
• appos : DepRel
• nummod : DepRel
• acl : DepRel
• amod : DepRel
• advmod : DepRel
• discourse : DepRel
• aux : DepRel
• auxPass : DepRel
• cop : DepRel
• mark : DepRel
• det : DepRel
• clf : DepRel
• case_ : DepRel
• compound : DepRel
• flat : DepRel
• fixed : DepRel
• list : DepRel
• parataxis : DepRel
• orphan : DepRel
• goesWith : DepRel
• reparandum : DepRel
• conj : DepRel
• cc : DepRel
• punct : DepRel
• root : DepRel
• dep : DepRel

@[implicit_reducible]

instance UD.instDecidableEqDepRel : DecidableEq DepRel

Equations

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

@[implicit_reducible]

instance UD.instReprDepRel : Repr DepRel

Equations

• UD.instReprDepRel = { reprPrec := UD.instReprDepRel.repr }

def UD.instReprDepRel.repr : DepRel → ℕ → Std.Format

Equations

• UD.instReprDepRel.repr UD.DepRel.nsubj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.nsubj")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.nsubjPass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.nsubjPass")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.csubj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.csubj")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.csubjPass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.csubjPass")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.obj")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.iobj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.iobj")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.ccomp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.ccomp")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.xcomp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.xcomp")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.obl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.obl")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.vocative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.vocative")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.expl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.expl")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.dislocated prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.dislocated")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.advcl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.advcl")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.nmod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.nmod")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.appos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.appos")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.nummod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.nummod")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.acl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.acl")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.amod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.amod")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.advmod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.advmod")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.discourse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.discourse")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.aux prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.aux")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.auxPass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.auxPass")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.cop prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.cop")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.mark prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.mark")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.det prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.det")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.clf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.clf")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.case_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.case_")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.compound prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.compound")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.flat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.flat")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.fixed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.fixed")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.list prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.list")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.parataxis prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.parataxis")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.orphan prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.orphan")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.goesWith prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.goesWith")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.reparandum prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.reparandum")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.conj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.conj")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.cc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.cc")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.punct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.punct")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.root prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.root")).group prec✝
• UD.instReprDepRel.repr UD.DepRel.dep prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.DepRel.dep")).group prec✝

@[implicit_reducible]

instance UD.instInhabitedDepRel : Inhabited DepRel

Equations

• UD.instInhabitedDepRel = { default := UD.instInhabitedDepRel.default }

def UD.DepRel.toString : DepRel → String

String representation matching UD conventions

Equations

• UD.DepRel.nsubj.toString = "nsubj"
• UD.DepRel.nsubjPass.toString = "nsubj:pass"
• UD.DepRel.csubj.toString = "csubj"
• UD.DepRel.csubjPass.toString = "csubj:pass"
• UD.DepRel.obj.toString = "obj"
• UD.DepRel.iobj.toString = "iobj"
• UD.DepRel.ccomp.toString = "ccomp"
• UD.DepRel.xcomp.toString = "xcomp"
• UD.DepRel.obl.toString = "obl"
• UD.DepRel.vocative.toString = "vocative"
• UD.DepRel.expl.toString = "expl"
• UD.DepRel.dislocated.toString = "dislocated"
• UD.DepRel.advcl.toString = "advcl"
• UD.DepRel.nmod.toString = "nmod"
• UD.DepRel.appos.toString = "appos"
• UD.DepRel.nummod.toString = "nummod"
• UD.DepRel.acl.toString = "acl"
• UD.DepRel.amod.toString = "amod"
• UD.DepRel.advmod.toString = "advmod"
• UD.DepRel.discourse.toString = "discourse"
• UD.DepRel.aux.toString = "aux"
• UD.DepRel.auxPass.toString = "aux:pass"
• UD.DepRel.cop.toString = "cop"
• UD.DepRel.mark.toString = "mark"
• UD.DepRel.det.toString = "det"
• UD.DepRel.clf.toString = "clf"
• UD.DepRel.case_.toString = "case"
• UD.DepRel.compound.toString = "compound"
• UD.DepRel.flat.toString = "flat"
• UD.DepRel.fixed.toString = "fixed"
• UD.DepRel.list.toString = "list"
• UD.DepRel.parataxis.toString = "parataxis"
• UD.DepRel.orphan.toString = "orphan"
• UD.DepRel.goesWith.toString = "goeswith"
• UD.DepRel.reparandum.toString = "reparandum"
• UD.DepRel.conj.toString = "conj"
• UD.DepRel.cc.toString = "cc"
• UD.DepRel.punct.toString = "punct"
• UD.DepRel.root.toString = "root"
• UD.DepRel.dep.toString = "dep"

@[implicit_reducible]

instance UD.instToStringDepRel : ToString DepRel

Equations

• UD.instToStringDepRel = { toString := UD.DepRel.toString }

def UD.DepRel.isCoreArg : DepRel → Bool

Is this a core argument relation?

Equations

• UD.DepRel.nsubj.isCoreArg = true
• UD.DepRel.nsubjPass.isCoreArg = true
• UD.DepRel.csubj.isCoreArg = true
• UD.DepRel.csubjPass.isCoreArg = true
• UD.DepRel.obj.isCoreArg = true
• UD.DepRel.iobj.isCoreArg = true
• UD.DepRel.ccomp.isCoreArg = true
• UD.DepRel.xcomp.isCoreArg = true
• x✝.isCoreArg = false

def UD.DepRel.isValencyArg : DepRel → Bool

Is this a valency-bearing dependency? Extends isCoreArg with .obl (oblique nominals), which valency frameworks (e.g. [OL23] on dependency-grammar valent typology) treat as a valency role even though UD classifies it as non-core.

Equations

• UD.DepRel.nsubj.isValencyArg = true
• UD.DepRel.nsubjPass.isValencyArg = true
• UD.DepRel.csubj.isValencyArg = true
• UD.DepRel.csubjPass.isValencyArg = true
• UD.DepRel.obj.isValencyArg = true
• UD.DepRel.iobj.isValencyArg = true
• UD.DepRel.ccomp.isValencyArg = true
• UD.DepRel.xcomp.isValencyArg = true
• UD.DepRel.obl.isValencyArg = true
• x✝.isValencyArg = false

def UD.DepRel.isSubject : DepRel → Bool

Is this a subject relation?

Equations

• UD.DepRel.nsubj.isSubject = true
• UD.DepRel.nsubjPass.isSubject = true
• UD.DepRel.csubj.isSubject = true
• UD.DepRel.csubjPass.isSubject = true
• x✝.isSubject = false

def UD.DepRel.isObject : DepRel → Bool

Is this an object relation?

Equations

• UD.DepRel.obj.isObject = true
• UD.DepRel.iobj.isObject = true
• x✝.isObject = false

def UD.DepRel.isModifier : DepRel → Bool

Is this a modifier relation?

Equations

• UD.DepRel.amod.isModifier = true
• UD.DepRel.advmod.isModifier = true
• UD.DepRel.nmod.isModifier = true
• UD.DepRel.nummod.isModifier = true
• UD.DepRel.advcl.isModifier = true
• UD.DepRel.acl.isModifier = true
• x✝.isModifier = false

def UD.DepRel.isFunctionWord : DepRel → Bool

Is this a function word relation?

Equations

• UD.DepRel.aux.isFunctionWord = true
• UD.DepRel.auxPass.isFunctionWord = true
• UD.DepRel.cop.isFunctionWord = true
• UD.DepRel.mark.isFunctionWord = true
• UD.DepRel.det.isFunctionWord = true
• UD.DepRel.case_.isFunctionWord = true
• UD.DepRel.clf.isFunctionWord = true
• x✝.isFunctionWord = false

structure UD.DepArc : Type

A single dependency arc in a UD tree

• dependent : ℕ

  Index of the dependent word (1-indexed)

• head : ℕ

  Index of the head word (0 = root)

• deprel : DepRel

  The dependency relation

def UD.instDecidableEqDepArc.decEq (x✝ x✝¹ : DepArc) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance UD.instDecidableEqDepArc : DecidableEq DepArc

Equations

• UD.instDecidableEqDepArc = UD.instDecidableEqDepArc.decEq

def UD.instReprDepArc.repr : DepArc → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance UD.instReprDepArc : Repr DepArc

Equations

• UD.instReprDepArc = { reprPrec := UD.instReprDepArc.repr }