Reciprocal pronouns — the pronominal exponent of reciprocity

The pronoun member of the reciprocal series: ReciprocalPronoun extends the general Pronoun with the marker data of Syntax/Reciprocal.lean, the nominal strategy it realizes and the readings it covers, and fixes the Principle-A reciprocal binding class. A fragment writes the pronoun once and derives its Reciprocal.Marker entry with toMarker; Hungarian egymás, Japanese otagai and Wan ɔ̄ŋ̄ are such objects. Verbal and clitic reciprocal strategies are not pronouns and stay bare markers.

Main declarations

• ReciprocalPronoun — the lexical object (extends Pronoun + strategy + readings).
• ReciprocalPronoun.toMarker — its entry in a marker inventory.
• HasPhi / Proform / Bound instances routing the object through the Pronoun API.

structure ReciprocalPronounextends Pronoun : Type

A reciprocal pronoun: the general Pronoun (surface form + φ-features) as the nominal exponent of reciprocity, with the strategy it realizes and the readings it covers. The kind fixes the Principle-A reciprocal binding class, so entries need not restate it.

• 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
• strategy : Reciprocal.Strategy

  The nominal strategy: a dedicated pronoun (egymás, otagai) or a bipartite quantifier NP (each other).

• readings : List Reciprocal.Reading

  The readings the form covers.

def instReprReciprocalPronoun.repr : ReciprocalPronoun → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprReciprocalPronoun : Repr ReciprocalPronoun

Equations

• instReprReciprocalPronoun = { reprPrec := instReprReciprocalPronoun.repr }

def instDecidableEqReciprocalPronoun.decEq (x✝ x✝¹ : ReciprocalPronoun) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqReciprocalPronoun : DecidableEq ReciprocalPronoun

Equations

• instDecidableEqReciprocalPronoun = instDecidableEqReciprocalPronoun.decEq

def ReciprocalPronoun.toMarker (p : ReciprocalPronoun) : Reciprocal.Marker

The marker entry of a reciprocal pronoun.

Equations

• p.toMarker = { form := p.form, script := p.script, strategy := p.strategy, readings := p.readings }

@[instance_reducible]

instance instHasPhiReciprocalPronoun : HasPhi ReciprocalPronoun

A reciprocal pronoun bears φ via its Pronoun core.

Equations

• instHasPhiReciprocalPronoun = { phi := fun (p : ReciprocalPronoun) => p.toWord.phi }

@[instance_reducible]

instance instProformReciprocalPronoun : Proform ReciprocalPronoun

Equations

• instProformReciprocalPronoun = { Domain := fun (p : ReciprocalPronoun) => Proform.Domain p.toPronoun }

@[instance_reducible]

instance instBoundReciprocalPronoun : Bound ReciprocalPronoun

Its binding class is the Pronoun core's, defaulting to the reciprocal.

Equations

• instBoundReciprocalPronoun = { bindingClass := fun (p : ReciprocalPronoun) => p.bindingClass.getD Features.BindingClass.reciprocal }