Numeral — the lexical numeral object

Theory-neutral lexical core for numerals: the substrate a Fragment instantiates and a semantics later interprets. A numeral word contributes a Comparison (the relation it draws — bare / at-least / more-than / …) and a numeric argument. The measure it compares against (cardinality, height, cost) is supplied compositionally, so it is not a lexical field here.

The comparison vocabulary itself is not numeral-specific — it is the shared degree-comparison primitive Core.Order.Comparison (also used by measure phrases and gradable comparatives, per [Ken15], [Ret14]); this file just records that a numeral entry carries one. The denotation (the Comparison.over-based meaning, the Kennedy-vs-Horn bare-form choice) lives in Semantics/Numerals/, which imports this object — the same object/denotation split as Syntax/Pronoun/Basic.lean vs. Semantics/Reference/PronounDenotation.lean.

Main declarations

• Numeral.Entry — cross-linguistic lexical numeral entry (form, comparison, argument).

structure Numeral.Entry : Type

Cross-linguistic lexical numeral entry: surface form, the Comparison it expresses, and its numeric argument. The measure compared against (cardinality, height, …) is compositional, supplied at denotation time rather than stored here.

• form : String

  Surface form (romanization or orthographic).

• comparison : Core.Order.Comparison

  The comparison the numeral expresses (bare or a modifier).

• argument : ℕ

  The numeric argument: the m in "more than m", "exactly m", …

def Numeral.instReprEntry.repr : Entry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Numeral.instReprEntry : Repr Entry

Equations

• Numeral.instReprEntry = { reprPrec := Numeral.instReprEntry.repr }

def Numeral.instDecidableEqEntry.decEq (x✝ x✝¹ : Entry) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Numeral.instDecidableEqEntry : DecidableEq Entry

Equations

• Numeral.instDecidableEqEntry = Numeral.instDecidableEqEntry.decEq