Romanian noun gender

Agreeing adjectives such as bun 'good' show two forms in the singular, -Ø and -ă, and two in the plural, -i and -e, but nouns fall into three sets by the forms they take across the two numbers: bărbat 'man' (-Ø, -i), fată 'girl' (-ă, -e) and scaun 'chair' (-Ø, -e), the last the disputed neuter or ambigeneric gender (Mallinson; Corbett).

References

• G. Mallinson, Rumanian (1984)
• G. G. Corbett, Gender (1991)

inductive Romanian.Gender.Value : Type

The three controller genders.

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

@[instance_reducible]

instance Romanian.Gender.instDecidableEqValue : DecidableEq Value

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Romanian.Gender.instReprValue.repr Romanian.Gender.Value.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Romanian.Gender.Value.fem")).group prec✝

@[instance_reducible]

instance Romanian.Gender.instReprValue : Repr Value

Equations

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

@[instance_reducible]

instance Romanian.Gender.instFintypeValue : Fintype Value

Equations

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

structure Romanian.Gender.Nounextends GenderedNoun Romanian.Gender.Value : Type

A Romanian noun with its controller gender, the gender it restricts its referents to where it does, and their animacy.

• form : String
• gloss : String
• gender : Romanian.Gender.Value
• referentGender : Option ReferentGender
• animacy : Animacy

  The animacy of the noun's referents.

@[instance_reducible]

instance Romanian.Gender.instDecidableEqNoun : DecidableEq Noun

Equations

• Romanian.Gender.instDecidableEqNoun = Romanian.Gender.instDecidableEqNoun.decEq

def Romanian.Gender.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

def Romanian.Gender.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Romanian.Gender.instReprNoun : Repr Noun

Equations

• Romanian.Gender.instReprNoun = { reprPrec := Romanian.Gender.instReprNoun.repr }

def Romanian.Gender.barbat : Noun

Equations

• Romanian.Gender.barbat = { form := "bărbat", gloss := "man", gender := Romanian.Gender.Value.masc, referentGender := some ReferentGender.male, animacy := Animacy.human }

def Romanian.Gender.fata : Noun

Equations

• Romanian.Gender.fata = { form := "fată", gloss := "girl", gender := Romanian.Gender.Value.fem, referentGender := some ReferentGender.female, animacy := Animacy.human }

def Romanian.Gender.scaun : Noun

Equations

• Romanian.Gender.scaun = { form := "scaun", gloss := "chair", gender := Romanian.Gender.Value.neut, animacy := Animacy.inanimate }

def Romanian.Gender.femeie : Noun

Equations

• Romanian.Gender.femeie = { form := "femeie", gloss := "woman", gender := Romanian.Gender.Value.fem, referentGender := some ReferentGender.female, animacy := Animacy.human }

def Romanian.Gender.baiat : Noun

Equations

• Romanian.Gender.baiat = { form := "băiat", gloss := "boy", gender := Romanian.Gender.Value.masc, referentGender := some ReferentGender.male, animacy := Animacy.human }

def Romanian.Gender.usa : Noun

Equations

• Romanian.Gender.usa = { form := "uşă", gloss := "door", gender := Romanian.Gender.Value.fem, animacy := Animacy.inanimate }

def Romanian.Gender.perete : Noun

Equations

• Romanian.Gender.perete = { form := "perete", gloss := "wall", gender := Romanian.Gender.Value.masc, animacy := Animacy.inanimate }

def Romanian.Gender.masa : Noun

Equations

• Romanian.Gender.masa = { form := "masă", gloss := "table", gender := Romanian.Gender.Value.fem, animacy := Animacy.inanimate }

def Romanian.Gender.nuc : Noun

Equations

• Romanian.Gender.nuc = { form := "nuc", gloss := "walnut tree", gender := Romanian.Gender.Value.masc, animacy := Animacy.inanimate }

def Romanian.Gender.prun : Noun

Equations

• Romanian.Gender.prun = { form := "prun", gloss := "plum tree", gender := Romanian.Gender.Value.masc, animacy := Animacy.inanimate }

def Romanian.Gender.frigider : Noun

Equations

• Romanian.Gender.frigider = { form := "frigider", gloss := "refrigerator", gender := Romanian.Gender.Value.neut, animacy := Animacy.inanimate }

def Romanian.Gender.televizor : Noun

Equations

• Romanian.Gender.televizor = { form := "televizor", gloss := "television", gender := Romanian.Gender.Value.neut, animacy := Animacy.inanimate }

def Romanian.Gender.allNouns : List Noun

Equations

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

inductive Romanian.Gender.AdjForm : Type

The endings of bun 'good'.

• zero : AdjForm
• ă : AdjForm
• i : AdjForm
• e : AdjForm

@[instance_reducible]

instance Romanian.Gender.instDecidableEqAdjForm : DecidableEq AdjForm

Equations

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

@[instance_reducible]

instance Romanian.Gender.instReprAdjForm : Repr AdjForm

Equations

• Romanian.Gender.instReprAdjForm = { reprPrec := Romanian.Gender.instReprAdjForm.repr }

def Romanian.Gender.instReprAdjForm.repr : AdjForm → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Romanian.Gender.instFintypeAdjForm : Fintype AdjForm

Equations

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

def Romanian.Gender.numberSystem : Number.System

Romanian distinguishes the singular and the plural.

Equations

• Romanian.Gender.numberSystem = Number.System.singularPlural

def Romanian.Gender.Value.adjForm (g : Value) : ↥numberSystem.values → AdjForm

The ending an agreeing adjective takes with each gender, in each number.

Equations

• Romanian.Gender.Value.masc.adjForm = Romanian.Gender.numberSystem.elim Romanian.Gender.AdjForm.zero Romanian.Gender.AdjForm.i Romanian.Gender.Value.adjForm._proof_3
• Romanian.Gender.Value.fem.adjForm = Romanian.Gender.numberSystem.elim Romanian.Gender.AdjForm.ă Romanian.Gender.AdjForm.e Romanian.Gender.Value.adjForm._proof_3
• Romanian.Gender.Value.neut.adjForm = Romanian.Gender.numberSystem.elim Romanian.Gender.AdjForm.zero Romanian.Gender.AdjForm.e Romanian.Gender.Value.adjForm._proof_3

theorem Romanian.Gender.faithful_adjForm : Gender.Faithful Value.adjForm