Person — carrier capabilities

[Cys09]

The typeclass mixin for carriers that bear grammatical person — the person analogue of HasNumber (Features/Number/Capabilities.lean). personOf extracts the carrier's analytical person value; Compatible is the agreement-checking relation. Carriers that store UD realization (UD.MorphFeatures) lift through Person.fromUD; carriers that store a (UD person, clusivity) pair recover the quadripartition cell (Syntax/Pronoun/Capabilities.lean).

class HasPerson (α : Type u_1) : Type u_1

A carrier of grammatical person. none = the carrier does not mark person.

• personOf : α → Option Person

  The analytical person value, if marked.

@[implicit_reducible]

instance instHasPersonMorphFeatures : HasPerson UD.MorphFeatures

Equations

• instHasPersonMorphFeatures = { personOf := fun (mf : UD.MorphFeatures) => Option.map Person.fromUD mf.person }

@[implicit_reducible]

instance instHasPersonPerson : HasPerson Person

Equations

• instHasPersonPerson = { personOf := some }

@[reducible, inline]

abbrev HasPerson.Compatible {α : Type u_1} {β : Type u_2} [HasPerson α] [HasPerson β] (a : α) (b : β) : Prop

Two carriers are person-compatible: the slot values are compatible in the flat information order (Compat) — if both mark person, the values agree; unmarked carriers are wildcards.

Equations

• HasPerson.Compatible a b = Compat (personOf a) (personOf b)

theorem UD.MorphFeatures.compatible_hasPerson {f1 f2 : MorphFeatures} (h : f1.compatible f2 = true) : HasPerson.Compatible f1 f2

φ-compatibility entails person compatibility: the HasPerson mixin never diverges from the unification-based agreement engine (UD.MorphFeatures.compatible) — the person analogue of UD.MorphFeatures.compatible_hasNumber.