English nouns

The English noun as a lexical entry: the root Noun with the mass/count feature, its lexical gender where it has one, and its plural where that is not the regular -s one, which Inflection.lean's suffixS supplies; names are the root ProperName. English nouns have no grammatical gender; the label recorded for man, woman and the names is the natural gender their pronouns agree with. Bare plurals and bare mass nouns are arguments and a bare singular count noun is not, which [chierchia-1998] derives from the Nominal Mapping Parameter (Studies/Chierchia1998.lean).

Main definitions

• Noun — the entry, with Noun.realize giving its form at a number
• Noun.toWordSg, Noun.toWord — the entry as a Word token

References

• [chierchia-1998]
• [krifka-2026]

structure English.Nouns.Nounextends Noun : Type

An English noun: the root entry with the mass/count feature, its lexical gender where it has one, and its plural where that is not the regular -s one.

• form : String
• gloss : String
• countable : MassCount

  The mass/count feature ([krifka-2026]).

• gender : Option Gender

  The natural gender the noun's pronouns agree with, where it has one.

• irregularPlural : Option String

  The plural, where it is not the regular -s one.

@[instance_reducible]

instance English.Nouns.instDecidableEqNoun : DecidableEq Noun

Equations

• English.Nouns.instDecidableEqNoun = English.Nouns.instDecidableEqNoun.decEq

def English.Nouns.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance English.Nouns.instReprNoun : Repr Noun

Equations

• English.Nouns.instReprNoun = { reprPrec := English.Nouns.instReprNoun.repr }

def English.Nouns.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

def English.Nouns.Noun.common (form : String) : Noun

A common count noun; English is the metalanguage, so the gloss is the form.

Equations

• English.Nouns.Noun.common form = { form := form, gloss := form }

def English.Nouns.Noun.mass (form : String) : Noun

A mass noun.

Equations

• English.Nouns.Noun.mass form = { form := form, gloss := form, countable := MassCount.mass }

def English.Nouns.Noun.realize (n : Noun) : Number → Option String

The form at a number: the citation form in the singular; in the plural, for a count noun, the irregular plural where there is one and else the regular -s one.

Equations

• n.realize Number.singular = some n.form
• n.realize Number.plural = if n.countable = MassCount.mass then none else some (n.irregularPlural.getD (English.Inflection.suffixS n.form))
• n.realize x✝ = none

def English.Nouns.Noun.toWordSg (n : Noun) : Morphology.Word

The singular as a word token: a NOUN with the gender where the entry has one.

Equations

• n.toWordSg = { form := n.form, cat := UD.UPOS.NOUN, features := Morphology.Features.of none (some Number.singular) n.gender }

def English.Nouns.Noun.toWord (n : Noun) (num : Number) : Option Morphology.Word

The entry as a word token at a number, where it has a form there.

Equations

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

theorem English.Nouns.Noun.toWord_singular (n : Noun) : n.toWord Number.singular = some n.toWordSg

Count nouns

def English.Nouns.pizza : Noun

Equations

• English.Nouns.pizza = English.Nouns.Noun.common "pizza"

def English.Nouns.book : Noun

Equations

• English.Nouns.book = English.Nouns.Noun.common "book"

def English.Nouns.cat : Noun

Equations

• English.Nouns.cat = English.Nouns.Noun.common "cat"

def English.Nouns.dog : Noun

Equations

• English.Nouns.dog = English.Nouns.Noun.common "dog"

def English.Nouns.girl : Noun

Equations

• English.Nouns.girl = English.Nouns.Noun.common "girl"

def English.Nouns.boy : Noun

Equations

• English.Nouns.boy = English.Nouns.Noun.common "boy"

def English.Nouns.ball : Noun

Equations

• English.Nouns.ball = English.Nouns.Noun.common "ball"

def English.Nouns.table : Noun

Equations

• English.Nouns.table = English.Nouns.Noun.common "table"

def English.Nouns.squirrel : Noun

Equations

• English.Nouns.squirrel = English.Nouns.Noun.common "squirrel"

def English.Nouns.kitchen : Noun

Equations

• English.Nouns.kitchen = English.Nouns.Noun.common "kitchen"

def English.Nouns.story : Noun

Equations

• English.Nouns.story = English.Nouns.Noun.common "story"

def English.Nouns.lawyer : Noun

Equations

• English.Nouns.lawyer = English.Nouns.Noun.common "lawyer"

def English.Nouns.student : Noun

Equations

• English.Nouns.student = English.Nouns.Noun.common "student"

def English.Nouns.teacher : Noun

Equations

• English.Nouns.teacher = English.Nouns.Noun.common "teacher"

def English.Nouns.soldier : Noun

Equations

• English.Nouns.soldier = English.Nouns.Noun.common "soldier"

def English.Nouns.horse : Noun

Equations

• English.Nouns.horse = English.Nouns.Noun.common "horse"

def English.Nouns.brother : Noun

Equations

• English.Nouns.brother = English.Nouns.Noun.common "brother"

def English.Nouns.spy : Noun

Equations

• English.Nouns.spy = English.Nouns.Noun.common "spy"

def English.Nouns.idea : Noun

Equations

• English.Nouns.idea = English.Nouns.Noun.common "idea"

def English.Nouns.lot : Noun

Equations

• English.Nouns.lot = English.Nouns.Noun.common "lot"

def English.Nouns.bean : Noun

Equations

• English.Nouns.bean = English.Nouns.Noun.common "bean"

def English.Nouns.father : Noun

Equations

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

def English.Nouns.mother : Noun

Equations

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

def English.Nouns.man : Noun

Equations

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

def English.Nouns.woman : Noun

Equations

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

def English.Nouns.fireman : Noun

Equations

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

def English.Nouns.person : Noun

Equations

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

def English.Nouns.child : Noun

Equations

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

Mass nouns

def English.Nouns.water : Noun

Equations

• English.Nouns.water = English.Nouns.Noun.mass "water"

def English.Nouns.sand : Noun

Equations

• English.Nouns.sand = English.Nouns.Noun.mass "sand"

def English.Nouns.trash : Noun

Equations

• English.Nouns.trash = English.Nouns.Noun.mass "trash"

def English.Nouns.furniture : Noun

Equations

• English.Nouns.furniture = English.Nouns.Noun.mass "furniture"

def English.Nouns.rice : Noun

Equations

• English.Nouns.rice = English.Nouns.Noun.mass "rice"

def English.Nouns.gold : Noun

Equations

• English.Nouns.gold = English.Nouns.Noun.mass "gold"

def English.Nouns.air : Noun

Equations

• English.Nouns.air = English.Nouns.Noun.mass "air"

def English.Nouns.wine : Noun

Equations

• English.Nouns.wine = English.Nouns.Noun.mass "wine"

def English.Nouns.coffee : Noun

Equations

• English.Nouns.coffee = English.Nouns.Noun.mass "coffee"

def English.Nouns.beer : Noun

Equations

• English.Nouns.beer = English.Nouns.Noun.mass "beer"

def English.Nouns.milk : Noun

Equations

• English.Nouns.milk = English.Nouns.Noun.mass "milk"

def English.Nouns.tea : Noun

Equations

• English.Nouns.tea = English.Nouns.Noun.mass "tea"

Proper names

def English.Nouns.name (form : String) (gender : Option Gender := none) : ProperName

A name glossed by itself.

Equations

• English.Nouns.name form gender = { form := form, gloss := form, gender := gender }

def English.Nouns.john : ProperName

Equations

• English.Nouns.john = English.Nouns.name "John" (some Gender.masculine)

def English.Nouns.mary : ProperName

Equations

• English.Nouns.mary = English.Nouns.name "Mary" (some Gender.feminine)

def English.Nouns.bill : ProperName

Equations

• English.Nouns.bill = English.Nouns.name "Bill" (some Gender.masculine)

def English.Nouns.sue : ProperName

Equations

• English.Nouns.sue = English.Nouns.name "Sue" (some Gender.feminine)

def English.Nouns.fred : ProperName

Equations

• English.Nouns.fred = English.Nouns.name "Fred" (some Gender.masculine)

def English.Nouns.sam : ProperName

Equations

• English.Nouns.sam = English.Nouns.name "Sam"

def English.Nouns.pat : ProperName

Equations

• English.Nouns.pat = English.Nouns.name "Pat"