Indefinite pronouns — the pronominal carrier of the indefinite series

[Has97]

The pronoun member of the cross-categorial indefinite series: IndefinitePronoun extends the general Pronoun (Syntax/Pronoun/Basic.lean) and carries the [Has97] series data (via Features/Indefinite.lean). A form like someone is one such object, instantiated in a Fragment, that flows through the Pronoun API like any other pronoun.

This is one carrier of the series, not its home: indefiniteness is word-class-neutral (the Indefinite capability and its feature taxonomy live in Features/Indefinite.lean). An indefinite determiner (some book) or pro-adverb (somewhere) would be a sibling carrier — a different word-class object supplying its own instance : Indefinite That — read by the same [Indefinite α] generic code. Cross-linguistic generalizations over indefinite pronouns (paradigm, WALS F46A bridge, syncretism) are typological and live in Typology/Indefinite.lean.

Main declarations

• Indefinite.IndefinitePronoun — the lexical object (extends Pronoun).
• instance : Indefinite Indefinite.IndefinitePronoun — the pronoun carrier of the series.
• Proform / Bound instances routing the object through the Pronoun API.

structure Indefinite.IndefinitePronounextends Pronoun : Type

A single indefinite pronoun — the canonical lexical object, extendsing the general Pronoun (surface form + φ-features) with the indefinite-series structure: its ontology-cal category ([Has97] §3.1.3), its morphological basis, and the functions it covers on the implicational map.

This is the single source of truth for an indefinite pronoun: it is a Pronoun, so it flows through the Pronoun API, and it carries its own distribution. functions is the realized cross-linguistic distribution (textbook-consensus data); theory-specific predictions about which functions a form should cover (Degano & Aloni 7-type team-semantics, choice-function denotation, Hamblin alternatives) are projections into theory-side types, not fields here.

• form : String
• person : Option Person
• number : Option Number
• case_ : Option Case
• gender : Option Gender
• script : Option String
• pronType : Option UD.PronType
• bindingClass : Option Features.BindingClass
• strength : Option Strength
• ontology : OntologicalCategory

  The [Has97] §3.1.3 ontological category (person, thing, …).

• basis : MorphologicalBasis

  The morphological derivation strategy (interrogative-based, etc.).

• functions : Finset HaspelmathFunction

  The functions on [Has97]'s implicational map this form covers (a contiguous region; see IndefiniteParadigm.AllContiguous).

def Indefinite.instDecidableEqIndefinitePronoun.decEq (x✝ x✝¹ : IndefinitePronoun) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Indefinite.instDecidableEqIndefinitePronoun : DecidableEq IndefinitePronoun

Equations

• Indefinite.instDecidableEqIndefinitePronoun = Indefinite.instDecidableEqIndefinitePronoun.decEq

@[implicit_reducible]

instance Indefinite.instReprIndefinitePronoun : Repr IndefinitePronoun

Manual Repr showing just the surface form to avoid the unsafe Repr (Finset α) instance from Mathlib.Data.Finset.Sort, which would propagate unsafety into every consumer of IndefinitePronoun.

Equations

• Indefinite.instReprIndefinitePronoun = { reprPrec := fun (e : Indefinite.IndefinitePronoun) (x : ℕ) => Std.Format.text (toString e.form) }

def Indefinite.IndefinitePronoun.covers (e : IndefinitePronoun) (f : HaspelmathFunction) : Bool

Does this entry cover function f?

Equations

• e.covers f = decide (f ∈ e.functions)

def Indefinite.IndefinitePronoun.functionList (e : IndefinitePronoun) : List HaspelmathFunction

For each form, the list of functions it covers, in HaspelmathFunction.all order.

Equations

• e.functionList = List.filter (fun (x : Indefinite.HaspelmathFunction) => e.covers x) Indefinite.HaspelmathFunction.all

def Indefinite.IndefinitePronoun.coverage (e : IndefinitePronoun) : ℕ

Coverage of a single form: number of functions it spans.

Equations

• e.coverage = e.functionList.length

Capability instances

@[implicit_reducible]

instance instProformIndefinitePronoun : Proform Indefinite.IndefinitePronoun

The indefinite pronoun is a Proform (form + φ via its Pronoun core).

Equations

• instProformIndefinitePronoun = { form := fun (e : Indefinite.IndefinitePronoun) => e.form, phi := fun (e : Indefinite.IndefinitePronoun) => e.toWord.phi }

@[implicit_reducible]

instance instBoundIndefinitePronoun : Bound Indefinite.IndefinitePronoun

An indefinite pronoun is a Principle-B pronominal (its Pronoun core's class, defaulting an undeclared φ-shell to .pronoun).

Equations

• instBoundIndefinitePronoun = { bindingClass := fun (e : Indefinite.IndefinitePronoun) => e.bindingClass.getD Features.BindingClass.pronoun }

@[implicit_reducible]

instance instIndefiniteIndefinitePronoun : Indefinite Indefinite.IndefinitePronoun

The indefinite pronoun is the pronominal carrier of the indefinite series.

Equations

• instIndefiniteIndefinitePronoun = { ontology := Indefinite.IndefinitePronoun.ontology, basis := Indefinite.IndefinitePronoun.basis, functions := Indefinite.IndefinitePronoun.functions }