Agreement tables as ordered-cell paradigms

The descriptive agreement table (Agreement.Paradigm, keyed by person/number/gender cells) and the theoretical ordered-cell object (Morphology.Paradigm n F, indexed by Fin n) are the same data under a choice of cell ordering. toParadigm transports the former onto the latter, reading off each ordered cell's exponent.

Main declarations

• Agreement.Paradigm.toParadigm — transport a cell-keyed table onto the n-cell ordered paradigm along an indexing Fin n → Agreement.Cell

def Agreement.Paradigm.toParadigm {Exp : Type u_1} [DecidableEq Exp] {n : ℕ} (e : Fin n → Cell) (p : Paradigm Exp) : Morphology.Paradigm n (Option Exp)

Transport a descriptive agreement table onto the ordered-cell Morphology.Paradigm: given an indexing e of the n ordered cells by agreement-feature cells, read off each cell's exponent (none where the table is defective for that cell).

Equations

• Agreement.Paradigm.toParadigm e p i = p.realize (e i)

@[simp]

theorem Agreement.Paradigm.toParadigm_apply {Exp : Type u_1} [DecidableEq Exp] {n : ℕ} (e : Fin n → Cell) (p : Paradigm Exp) (i : Fin n) : toParadigm e p i = p.realize (e i)