Universal Dependencies: morphological features

[dMMNZ21]

The morphological feature tags of UD v2, nominal, pronominal and verbal, and the annotation record MorphFeatures, a tag or ⊥ in each feature. The analytical inventories of person, number, gender and case realize as these tags and ingest from them in Morphology/Word/UD.lean; the remaining tags serve as the value types of a token's features until an analytical inventory exists.

Official site: https://universaldependencies.org/

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

@[instance_reducible]

instance UD.instDecidableEqNumber : DecidableEq Number

Equations

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

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✝

@[instance_reducible]

instance UD.instReprNumber : Repr Number

Equations

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

@[instance_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

@[instance_reducible]

instance UD.instDecidableEqGender : DecidableEq Gender

Equations

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

@[instance_reducible]

instance UD.instReprGender : Repr Gender

Equations

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

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✝

@[instance_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 (Syntax/Case/Basic.lean), realized and ingested in Morphology/Word/UD.lean.

• 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

@[instance_reducible]

instance UD.instDecidableEqCase : DecidableEq Case

Equations

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

@[instance_reducible]

instance UD.instReprCase : Repr Case

Equations

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

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✝

@[instance_reducible]

instance UD.instInhabitedCase : Inhabited Case

Equations

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

@[instance_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

@[instance_reducible]

instance UD.instDecidableEqDefinite : DecidableEq Definite

Equations

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

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✝

@[instance_reducible]

instance UD.instReprDefinite : Repr Definite

Equations

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

@[instance_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

@[instance_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✝

@[instance_reducible]

instance UD.instReprDegree : Repr Degree

Equations

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

@[instance_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

@[instance_reducible]

instance UD.instDecidableEqPronType : DecidableEq PronType

Equations

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

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✝

@[instance_reducible]

instance UD.instReprPronType : Repr PronType

Equations

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

@[instance_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

@[instance_reducible]

instance UD.instDecidableEqPerson : DecidableEq Person

Equations

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

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✝

@[instance_reducible]

instance UD.instReprPerson : Repr Person

Equations

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

@[instance_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

@[instance_reducible]

instance UD.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

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

@[instance_reducible]

instance UD.instReprVerbForm : Repr VerbForm

Equations

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

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✝

@[instance_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

@[instance_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✝

@[instance_reducible]

instance UD.instReprTense : Repr Tense

Equations

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

@[instance_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

@[instance_reducible]

instance UD.instDecidableEqAspect : DecidableEq Aspect

Equations

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

@[instance_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✝

@[instance_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

@[instance_reducible]

instance UD.instDecidableEqMood : DecidableEq Mood

Equations

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

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✝

@[instance_reducible]

instance UD.instReprMood : Repr Mood

Equations

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

@[instance_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

@[instance_reducible]

instance UD.instDecidableEqVoice : DecidableEq Voice

Equations

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

@[instance_reducible]

instance UD.instReprVoice : Repr Voice

Equations

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

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✝

@[instance_reducible]

instance UD.instInhabitedVoice : Inhabited Voice

Equations

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

inductive UD.Polarity : Type

Polarity

• Pos : Polarity
• Neg : Polarity

@[instance_reducible]

instance UD.instDecidableEqPolarity : DecidableEq Polarity

Equations

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

@[instance_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✝

@[instance_reducible]

instance UD.instInhabitedPolarity : Inhabited Polarity

Equations

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

structure UD.MorphFeatures : Type

A morphological annotation record, a tag or ⊥ in each feature.

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

  Reflexive, Reflex=Yes; false when the feature is absent.

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

@[instance_reducible]

instance UD.instDecidableEqMorphFeatures : DecidableEq MorphFeatures

Equations

• UD.instDecidableEqMorphFeatures = UD.instDecidableEqMorphFeatures.decEq

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

Equations

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

@[instance_reducible]

instance UD.instReprMorphFeatures : Repr MorphFeatures

Equations

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

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

Equations

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

@[instance_reducible]

instance UD.instInhabitedMorphFeatures : Inhabited MorphFeatures

Equations

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