Interrogative pronouns

An interrogative pronoun is a pronoun with the ontological category it asks about: a person for who, a thing for what, a place for where. The categories are those of the indefinite series, which many languages build on their interrogatives, and they take in the pro-forms for place, time and manner, which surface as adverbs.

Main definitions

• InterrogativePronoun: a pronoun with its ontological category.
• InterrogativePronoun.toWord: its token, wh-marked (InterrogativePronoun.isWh_toWord).

References

• [Has97]

structure InterrogativePronounextends Pronoun : Type

An interrogative pronoun is a Pronoun with the ontological category it asks about.

• form : String
• person : Option Person
• number : Option Number
• case_ : Option Case
• gender : Option Gender
• script : Option String
• strength : Option Strength
• ontology : Pronoun.OntologicalCategory

  The ontological category the form asks about.

def instDecidableEqInterrogativePronoun.decEq (x✝ x✝¹ : InterrogativePronoun) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqInterrogativePronoun : DecidableEq InterrogativePronoun

Equations

• instDecidableEqInterrogativePronoun = instDecidableEqInterrogativePronoun.decEq

def instReprInterrogativePronoun.repr : InterrogativePronoun → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprInterrogativePronoun : Repr InterrogativePronoun

Equations

• instReprInterrogativePronoun = { reprPrec := instReprInterrogativePronoun.repr }

def InterrogativePronoun.toWord (p : InterrogativePronoun) : Morphology.Word

An interrogative's word is of UD pronoun type Int, with the word class its category fixes.

Equations

• p.toWord = { form := (p.toWord (some UD.PronType.Int)).form, cat := p.ontology.upos, features := (p.toWord (some UD.PronType.Int)).features }

theorem InterrogativePronoun.isWh_toWord (p : InterrogativePronoun) : p.toWord.features.IsWh

An interrogative projects a wh-marked word.