Rules of exponence

This file defines the Exponence.Rule typeclass, pairing an exponent exponent : R → E with an applicability condition Applies : R → Ctx → Prop ([Mat91]), and the specificity preorder it induces.

Main definitions

• Exponence.Rule: the exponent-plus-applicability interface.
• Exponence.toPreorder: the specificity preorder ([Kip73]'s Elsewhere Condition); not an instance — each engine installs it on its own carrier.

class Morphology.Exponence.Rule (R : Type u_1) (Ctx : outParam (Type u_2)) (E : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

Rule R Ctx E says that R is a type of rules of exponence: each rule carries an exponent in E and applies in a class of contexts in Ctx.

• exponent : R → E

  The exponent a rule inserts.

• Applies : R → Ctx → Prop

  The condition on contexts under which a rule applies.

def Morphology.Exponence.applySet {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] (r : R) : Set Ctx

The contexts in which a rule applies.

Equations

• Morphology.Exponence.applySet r = {c : Ctx | Morphology.Exponence.Applies r c}

@[simp]

theorem Morphology.Exponence.mem_applySet {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] {r : R} {c : Ctx} : c ∈ applySet r ↔ Applies r c

@[reducible]

def Morphology.Exponence.toPreorder {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] : Preorder R

r ≤ s when r applies in a subset of the contexts s applies in.

Equations

• Morphology.Exponence.toPreorder = Preorder.lift Morphology.Exponence.applySet