Noun

The noun as a lexical entry: its citation form and its gloss, everything a noun of any language carries. A language with gender extends the entry with the controller gender in its own carrier, the gender the language's assignment rules give the noun, and with whether that gender follows the referent's sex, the one facet every system with a semantic core reads; the facets particular rules read besides, animacy, rationality, declension class or accent, are the fields of the fragments' further extensions. The general concept takes the plain name and the specializations extend it, as in mathlib; a gendered noun bears the comparative label its carrier does.

Implementation notes

• A fragment's extension is its own Noun, in its namespace; a file that opens that namespace qualifies the name, the root Noun being in scope too.

Main declarations

• Noun — the noun entry.
• GenderedNoun G — the entry with its controller gender over the carrier G.

structure Noun : Type

A noun entry: citation form and gloss.

• form : String

  The citation form.

• gloss : String

  The gloss.

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

Equations

• instDecidableEqNoun.decEq { form := a, gloss := a_1 } { form := b, gloss := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqNoun : DecidableEq Noun

Equations

• instDecidableEqNoun = instDecidableEqNoun.decEq

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

Equations

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

@[instance_reducible]

instance instReprNoun : Repr Noun

Equations

• instReprNoun = { reprPrec := instReprNoun.repr }

structure GenderedNoun (G : Type u_1) extends Noun : Type u_1

A noun with its controller gender over the carrier G, and whether that gender follows the referent's sex.

• form : String
• gloss : String
• gender : G

  The controller gender: the agreements the noun takes.

• isNaturalGender : Bool

  Whether the gender follows the referent's sex.

@[instance_reducible]

instance instDecidableEqGenderedNoun {G✝ : Type u_1} [DecidableEq G✝] : DecidableEq (GenderedNoun G✝)

Equations

• instDecidableEqGenderedNoun = instDecidableEqGenderedNoun.decEq

def instDecidableEqGenderedNoun.decEq {G✝ : Type u_1} [DecidableEq G✝] (x✝ x✝¹ : GenderedNoun G✝) : Decidable (x✝ = x✝¹)

Equations

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

def instReprGenderedNoun.repr {G✝ : Type u_1} [Repr G✝] : GenderedNoun G✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprGenderedNoun {G✝ : Type u_1} [Repr G✝] : Repr (GenderedNoun G✝)

Equations

• instReprGenderedNoun = { reprPrec := instReprGenderedNoun.repr }

@[instance_reducible]

instance instHasGenderGenderedNoun {G : Type u_1} [HasGender G] : HasGender (GenderedNoun G)

A gendered noun bears the comparative label of its gender.

Equations

• instHasGenderGenderedNoun = { genderOf := fun (n : GenderedNoun G) => genderOf n.gender }