Latin noun gender

Latin has three genders, masculine, feminine and neuter, and its adjectives differ in how many of them they distinguish: in the nominative singular acer 'sharp' has a form for each, facilis 'easy' sets the neuter against the other two, and felix 'happy' has one form for all three ([Cor98]).

References

• G. G. Corbett, Morphology and agreement (1998)

inductive Latin.Gender.Value : Type

The three controller genders.

• masc : Value
• fem : Value
• neut : Value

@[instance_reducible]

instance Latin.Gender.instDecidableEqValue : DecidableEq Value

Equations

• Latin.Gender.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Latin.Gender.instReprValue.repr : Value → ℕ → Std.Format

Equations

• Latin.Gender.instReprValue.repr Latin.Gender.Value.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Latin.Gender.Value.masc")).group prec✝
• Latin.Gender.instReprValue.repr Latin.Gender.Value.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Latin.Gender.Value.fem")).group prec✝
• Latin.Gender.instReprValue.repr Latin.Gender.Value.neut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Latin.Gender.Value.neut")).group prec✝

@[instance_reducible]

instance Latin.Gender.instReprValue : Repr Value

Equations

• Latin.Gender.instReprValue = { reprPrec := Latin.Gender.instReprValue.repr }

@[instance_reducible]

instance Latin.Gender.instFintypeValue : Fintype Value

Equations

• Latin.Gender.instFintypeValue = { elems := { val := ↑Latin.Gender.Value.enumList, nodup := Latin.Gender.Value.enumList_nodup }, complete := Latin.Gender.instFintypeValue._proof_1 }

structure Latin.Gender.Adjective : Type

An adjective by its nominative singular forms.

• gloss : String

  The gloss.

• nomSg : Value → String

  The nominative singular form in each gender.

def Latin.Gender.acer : Adjective

acer, acris, acre 'sharp'.

Equations

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

def Latin.Gender.facilis : Adjective

facilis, facile 'easy'.

Equations

• Latin.Gender.facilis = { gloss := "easy", nomSg := fun (x : Latin.Gender.Value) => match x with | Latin.Gender.Value.neut => "facile" | x => "facilis" }

def Latin.Gender.felix : Adjective

felix 'happy'.

Equations

• Latin.Gender.felix = { gloss := "happy", nomSg := fun (x : Latin.Gender.Value) => "felix" }

def Latin.Gender.allAdjectives : List Adjective

The adjectives of Corbett's table.

Equations

• Latin.Gender.allAdjectives = [Latin.Gender.acer, Latin.Gender.facilis, Latin.Gender.felix]

theorem Latin.Gender.faithful_acer : Function.Injective acer.nomSg

acer distinguishes all three genders in the nominative singular.