Spanish noun gender

Spanish nouns are masculine or feminine. A noun for a human being or one of a few well-known animals takes the gender of the referent's sex, el hombre 'man' and la mujer 'woman', in a special form for each sex, el rey, la reina, or with feminine -a for masculine -o, el gato, la gata; some such nouns have one form for either sex, el or la estudiante, and a few have one gender whatever the referent's sex, la persona 'person' and el ángel 'angel'. The gender of every other noun, for things, plants and the remaining animals, has nothing to do with sex and must be learned: la mesa 'table', el libro 'book'. The article and adjectives agree: -o with a masculine, -a with a feminine ([BBMR19]).

Main definitions

• Spanish.Gender.Value — the two genders, with their comparative labels
• Spanish.Gender.Noun, Spanish.Gender.allNouns — nouns with a fixed gender
• Spanish.Gender.eitherGender — nouns with one form for either sex

References

• [BBMR19]

inductive Spanish.Gender.Value : Type

The two genders.

• masc : Value
• fem : Value

@[instance_reducible]

instance Spanish.Gender.instDecidableEqValue : DecidableEq Value

Equations

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

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

Equations

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

@[instance_reducible]

instance Spanish.Gender.instReprValue : Repr Value

Equations

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

@[instance_reducible]

instance Spanish.Gender.instFintypeValue : Fintype Value

Equations

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

def Spanish.Gender.Value.toLabel : Value → Gender

The comparative label of each gender.

Equations

• Spanish.Gender.Value.masc.toLabel = Gender.masculine
• Spanish.Gender.Value.fem.toLabel = Gender.feminine

@[reducible, inline]

abbrev Spanish.Gender.Noun : Type

A noun with its gender and the gender of its referents where the gender is the referent's.

Equations

• Spanish.Gender.Noun = GenderedNoun Spanish.Gender.Value

Nouns taking the referent's gender

def Spanish.Gender.hombre : Noun

hombre 'man'.

Equations

• Spanish.Gender.hombre = { form := "hombre", gloss := "man", gender := Spanish.Gender.Value.masc, naturalGender := some Gender.masculine }

def Spanish.Gender.mujer : Noun

mujer 'woman'.

Equations

• Spanish.Gender.mujer = { form := "mujer", gloss := "woman", gender := Spanish.Gender.Value.fem, naturalGender := some Gender.feminine }

def Spanish.Gender.niño : Noun

niño 'boy'.

Equations

• Spanish.Gender.niño = { form := "niño", gloss := "boy", gender := Spanish.Gender.Value.masc, naturalGender := some Gender.masculine }

def Spanish.Gender.niña : Noun

niña 'girl'.

Equations

• Spanish.Gender.niña = { form := "niña", gloss := "girl", gender := Spanish.Gender.Value.fem, naturalGender := some Gender.feminine }

def Spanish.Gender.rey : Noun

rey 'king'.

Equations

• Spanish.Gender.rey = { form := "rey", gloss := "king", gender := Spanish.Gender.Value.masc, naturalGender := some Gender.masculine }

def Spanish.Gender.reina : Noun

reina 'queen'.

Equations

• Spanish.Gender.reina = { form := "reina", gloss := "queen", gender := Spanish.Gender.Value.fem, naturalGender := some Gender.feminine }

def Spanish.Gender.gato : Noun

gato 'cat', also for the species.

Equations

• Spanish.Gender.gato = { form := "gato", gloss := "cat", gender := Spanish.Gender.Value.masc, naturalGender := some Gender.masculine }

def Spanish.Gender.gata : Noun

gata 'she-cat'.

Equations

• Spanish.Gender.gata = { form := "gata", gloss := "she-cat", gender := Spanish.Gender.Value.fem, naturalGender := some Gender.feminine }

Nouns of one gender for either sex

def Spanish.Gender.persona : Noun

persona 'person', feminine whatever the referent's sex.

Equations

• Spanish.Gender.persona = { form := "persona", gloss := "person", gender := Spanish.Gender.Value.fem }

def Spanish.Gender.ángel : Noun

ángel 'angel', masculine whatever the referent's sex.

Equations

• Spanish.Gender.ángel = { form := "ángel", gloss := "angel", gender := Spanish.Gender.Value.masc }

Nouns of arbitrary gender

def Spanish.Gender.mesa : Noun

mesa 'table'.

Equations

• Spanish.Gender.mesa = { form := "mesa", gloss := "table", gender := Spanish.Gender.Value.fem }

def Spanish.Gender.silla : Noun

silla 'chair'.

Equations

• Spanish.Gender.silla = { form := "silla", gloss := "chair", gender := Spanish.Gender.Value.fem }

def Spanish.Gender.casa : Noun

casa 'house'.

Equations

• Spanish.Gender.casa = { form := "casa", gloss := "house", gender := Spanish.Gender.Value.fem }

def Spanish.Gender.puerta : Noun

puerta 'door'.

Equations

• Spanish.Gender.puerta = { form := "puerta", gloss := "door", gender := Spanish.Gender.Value.fem }

def Spanish.Gender.ventana : Noun

ventana 'window'.

Equations

• Spanish.Gender.ventana = { form := "ventana", gloss := "window", gender := Spanish.Gender.Value.fem }

def Spanish.Gender.cama : Noun

cama 'bed'.

Equations

• Spanish.Gender.cama = { form := "cama", gloss := "bed", gender := Spanish.Gender.Value.fem }

def Spanish.Gender.libro : Noun

libro 'book'.

Equations

• Spanish.Gender.libro = { form := "libro", gloss := "book", gender := Spanish.Gender.Value.masc }

def Spanish.Gender.zapato : Noun

zapato 'shoe'.

Equations

• Spanish.Gender.zapato = { form := "zapato", gloss := "shoe", gender := Spanish.Gender.Value.masc }

def Spanish.Gender.coche : Noun

coche 'car'.

Equations

• Spanish.Gender.coche = { form := "coche", gloss := "car", gender := Spanish.Gender.Value.masc }

def Spanish.Gender.árbol : Noun

árbol 'tree'.

Equations

• Spanish.Gender.árbol = { form := "árbol", gloss := "tree", gender := Spanish.Gender.Value.masc }

def Spanish.Gender.cielo : Noun

cielo 'sky'.

Equations

• Spanish.Gender.cielo = { form := "cielo", gloss := "sky", gender := Spanish.Gender.Value.masc }

def Spanish.Gender.vaso : Noun

vaso 'glass'.

Equations

• Spanish.Gender.vaso = { form := "vaso", gloss := "glass", gender := Spanish.Gender.Value.masc }

def Spanish.Gender.allNouns : List Noun

The nouns with a fixed gender.

Equations

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

Nouns of either gender

def Spanish.Gender.soldado : _root_.Noun

soldado 'soldier': un soldado, una soldado.

Equations

• Spanish.Gender.soldado = { form := "soldado", gloss := "soldier" }

def Spanish.Gender.estudiante : _root_.Noun

estudiante 'student': el estudiante, la estudiante.

Equations

• Spanish.Gender.estudiante = { form := "estudiante", gloss := "student" }

def Spanish.Gender.artista : _root_.Noun

artista 'artist': el artista, la artista.

Equations

• Spanish.Gender.artista = { form := "artista", gloss := "artist" }

def Spanish.Gender.eitherGender : List _root_.Noun

The nouns with one form for either sex, masculine of a male referent and feminine of a female one.

Equations

• Spanish.Gender.eitherGender = [Spanish.Gender.soldado, Spanish.Gender.estudiante, Spanish.Gender.artista]

Agreement

inductive Spanish.Gender.Concord : Type

The endings of an agreeing adjective.

• o : Concord
• a : Concord

@[instance_reducible]

instance Spanish.Gender.instDecidableEqConcord : DecidableEq Concord

Equations

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

def Spanish.Gender.instReprConcord.repr : Concord → ℕ → Std.Format

Equations

• Spanish.Gender.instReprConcord.repr Spanish.Gender.Concord.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spanish.Gender.Concord.o")).group prec✝
• Spanish.Gender.instReprConcord.repr Spanish.Gender.Concord.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spanish.Gender.Concord.a")).group prec✝

@[instance_reducible]

instance Spanish.Gender.instReprConcord : Repr Concord

Equations

• Spanish.Gender.instReprConcord = { reprPrec := Spanish.Gender.instReprConcord.repr }

def Spanish.Gender.Value.concord : Value → Concord

The ending an adjective takes in agreement with a gender.

Equations

• Spanish.Gender.Value.masc.concord = Spanish.Gender.Concord.o
• Spanish.Gender.Value.fem.concord = Spanish.Gender.Concord.a

theorem Spanish.Gender.faithful_concord : Function.Injective Value.concord

The genders are told apart by adjectival agreement.