structure Fragments.English.FunctionWords.PrepEntry : Type

• form : String
• passiveAgent : Bool

  Can introduce an agent in passive?

def Fragments.English.FunctionWords.instReprPrepEntry.repr : PrepEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.FunctionWords.instReprPrepEntry : Repr PrepEntry

Equations

• Fragments.English.FunctionWords.instReprPrepEntry = { reprPrec := Fragments.English.FunctionWords.instReprPrepEntry.repr }

instance Fragments.English.FunctionWords.instBEqPrepEntry : BEq PrepEntry

Equations

• Fragments.English.FunctionWords.instBEqPrepEntry = { beq := Fragments.English.FunctionWords.instBEqPrepEntry.beq }

def Fragments.English.FunctionWords.instBEqPrepEntry.beq : PrepEntry → PrepEntry → Bool

Equations

• Fragments.English.FunctionWords.instBEqPrepEntry.beq { form := a, passiveAgent := a_1 } { form := b, passiveAgent := b_1 } = (a == b && a_1 == b_1)
• Fragments.English.FunctionWords.instBEqPrepEntry.beq x✝¹ x✝ = false

def Fragments.English.FunctionWords.to_ : PrepEntry

Equations

• Fragments.English.FunctionWords.to_ = { form := "to" }

def Fragments.English.FunctionWords.on : PrepEntry

Equations

• Fragments.English.FunctionWords.on = { form := "on" }

def Fragments.English.FunctionWords.in_ : PrepEntry

Equations

• Fragments.English.FunctionWords.in_ = { form := "in" }

def Fragments.English.FunctionWords.at_ : PrepEntry

Equations

• Fragments.English.FunctionWords.at_ = { form := "at" }

def Fragments.English.FunctionWords.by_ : PrepEntry

Equations

• Fragments.English.FunctionWords.by_ = { form := "by", passiveAgent := true }

def Fragments.English.FunctionWords.with_ : PrepEntry

Equations

• Fragments.English.FunctionWords.with_ = { form := "with" }

def Fragments.English.FunctionWords.from_ : PrepEntry

Equations

• Fragments.English.FunctionWords.from_ = { form := "from" }

def Fragments.English.FunctionWords.before : PrepEntry

Equations

• Fragments.English.FunctionWords.before = { form := "before" }

def Fragments.English.FunctionWords.after : PrepEntry

Equations

• Fragments.English.FunctionWords.after = { form := "after" }

def Fragments.English.FunctionWords.allPrepositions : List PrepEntry

Equations

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

def Fragments.English.FunctionWords.PrepEntry.toWord (p : PrepEntry) : Word

Equations

• p.toWord = { form := p.form, cat := UD.UPOS.ADP }

structure Fragments.English.FunctionWords.CompEntry : Type

• form : String
• question : Bool

  Introduces a question?

• conditional : Bool

  Introduces a conditional?

• optional : Bool

  Can be omitted?

instance Fragments.English.FunctionWords.instReprCompEntry : Repr CompEntry

Equations

• Fragments.English.FunctionWords.instReprCompEntry = { reprPrec := Fragments.English.FunctionWords.instReprCompEntry.repr }

def Fragments.English.FunctionWords.instReprCompEntry.repr : CompEntry → ℕ → Std.Format

Equations

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

def Fragments.English.FunctionWords.instBEqCompEntry.beq : CompEntry → CompEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.FunctionWords.instBEqCompEntry.beq x✝¹ x✝ = false

instance Fragments.English.FunctionWords.instBEqCompEntry : BEq CompEntry

Equations

• Fragments.English.FunctionWords.instBEqCompEntry = { beq := Fragments.English.FunctionWords.instBEqCompEntry.beq }

def Fragments.English.FunctionWords.that : CompEntry

Equations

• Fragments.English.FunctionWords.that = { form := "that", optional := true }

def Fragments.English.FunctionWords.if_ : CompEntry

Equations

• Fragments.English.FunctionWords.if_ = { form := "if", question := true, conditional := true }

def Fragments.English.FunctionWords.whether : CompEntry

Equations

• Fragments.English.FunctionWords.whether = { form := "whether", question := true }

def Fragments.English.FunctionWords.because : CompEntry

Equations

• Fragments.English.FunctionWords.because = { form := "because" }

def Fragments.English.FunctionWords.although : CompEntry

Equations

• Fragments.English.FunctionWords.although = { form := "although" }

def Fragments.English.FunctionWords.while_ : CompEntry

Equations

• Fragments.English.FunctionWords.while_ = { form := "while" }

def Fragments.English.FunctionWords.allComplementizers : List CompEntry

Equations

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

def Fragments.English.FunctionWords.CompEntry.toWord (c : CompEntry) : Word

Equations

• c.toWord = { form := c.form, cat := UD.UPOS.SCONJ }

inductive Fragments.English.FunctionWords.AuxType : Type

Auxiliary type

• modal : AuxType
• doSupport : AuxType
• be : AuxType
• have : AuxType

instance Fragments.English.FunctionWords.instDecidableEqAuxType : DecidableEq AuxType

Equations

• Fragments.English.FunctionWords.instDecidableEqAuxType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.FunctionWords.instReprAuxType.repr : AuxType → ℕ → Std.Format

Equations

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

instance Fragments.English.FunctionWords.instReprAuxType : Repr AuxType

Equations

• Fragments.English.FunctionWords.instReprAuxType = { reprPrec := Fragments.English.FunctionWords.instReprAuxType.repr }

instance Fragments.English.FunctionWords.instBEqAuxType : BEq AuxType

Equations

• Fragments.English.FunctionWords.instBEqAuxType = { beq := Fragments.English.FunctionWords.instBEqAuxType.beq }

def Fragments.English.FunctionWords.instBEqAuxType.beq : AuxType → AuxType → Bool

Equations

• Fragments.English.FunctionWords.instBEqAuxType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Fragments.English.FunctionWords.AuxEntry : Type

• form : String
• auxType : AuxType
• person : Option Person

  Person/number agreement

• number : Option Number
• tense : Option UD.Tense

  Morphological tense. none for base forms (modals like can, will). Note: "past" modals (could, would) carry Past as a morphological feature even when semantically non-past (counterfactual, polite).

• modalMeaning : List Core.Modality.ForceFlavor

  Modal meaning in the force-flavor space (Imel, Guo, & @cite{imel-guo-steinert-threlkeld-2026}). Empty for non-modal auxiliaries.

• register : Core.Register.Level

  Register level. Formal items (must, shall) vs informal items (have to) vs unmarked (can, will).

• negForm : Option String

  Contracted negative form with -n't, if it exists. none for paradigm gaps (mayn't, amn't).

• negIrregular : Bool

  Phonological irregularity in the negative form (Z&P criterion C). true when the contracted form cannot be derived by regular -n't suffixation (e.g., won't ← will, can't ← can, don't ← do).

instance Fragments.English.FunctionWords.instReprAuxEntry : Repr AuxEntry

Equations

• Fragments.English.FunctionWords.instReprAuxEntry = { reprPrec := Fragments.English.FunctionWords.instReprAuxEntry.repr }

def Fragments.English.FunctionWords.instReprAuxEntry.repr : AuxEntry → ℕ → Std.Format

Equations

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

def Fragments.English.FunctionWords.instBEqAuxEntry.beq : AuxEntry → AuxEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.FunctionWords.instBEqAuxEntry.beq x✝¹ x✝ = false

instance Fragments.English.FunctionWords.instBEqAuxEntry : BEq AuxEntry

Equations

• Fragments.English.FunctionWords.instBEqAuxEntry = { beq := Fragments.English.FunctionWords.instBEqAuxEntry.beq }

def Fragments.English.FunctionWords.can : AuxEntry

Equations

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

def Fragments.English.FunctionWords.could : AuxEntry

Equations

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

def Fragments.English.FunctionWords.will : AuxEntry

Equations

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

def Fragments.English.FunctionWords.would : AuxEntry

Equations

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

def Fragments.English.FunctionWords.shall : AuxEntry

Equations

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

def Fragments.English.FunctionWords.should : AuxEntry

Equations

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

def Fragments.English.FunctionWords.may : AuxEntry

Equations

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

def Fragments.English.FunctionWords.might : AuxEntry

Equations

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

def Fragments.English.FunctionWords.must : AuxEntry

Equations

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

def Fragments.English.FunctionWords.haveTo : AuxEntry

Have to: periphrastic deontic/circumstantial necessity. Informal register variant of must. Inflects unlike true modals: has to, had to, having to.

Equations

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

def Fragments.English.FunctionWords.dare : AuxEntry

Equations

• Fragments.English.FunctionWords.dare = { form := "dare", auxType := Fragments.English.FunctionWords.AuxType.modal, negForm := some "daren't" }

def Fragments.English.FunctionWords.need : AuxEntry

Equations

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

def Fragments.English.FunctionWords.ought : AuxEntry

Equations

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

def Fragments.English.FunctionWords.do_ : AuxEntry

Equations

• Fragments.English.FunctionWords.do_ = { form := "do", auxType := Fragments.English.FunctionWords.AuxType.doSupport, number := some Number.pl, negForm := some "don't", negIrregular := true }

def Fragments.English.FunctionWords.does : AuxEntry

Equations

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

def Fragments.English.FunctionWords.did : AuxEntry

Equations

• Fragments.English.FunctionWords.did = { form := "did", auxType := Fragments.English.FunctionWords.AuxType.doSupport, tense := some UD.Tense.Past, negForm := some "didn't" }

def Fragments.English.FunctionWords.am : AuxEntry

Equations

• Fragments.English.FunctionWords.am = { form := "am", auxType := Fragments.English.FunctionWords.AuxType.be, person := some UD.Person.first, number := some Number.sg }

def Fragments.English.FunctionWords.is_ : AuxEntry

Equations

• Fragments.English.FunctionWords.is_ = { form := "is", auxType := Fragments.English.FunctionWords.AuxType.be, person := some UD.Person.third, number := some Number.sg, negForm := some "isn't" }

def Fragments.English.FunctionWords.are : AuxEntry

Equations

• Fragments.English.FunctionWords.are = { form := "are", auxType := Fragments.English.FunctionWords.AuxType.be, number := some Number.pl, negForm := some "aren't" }

def Fragments.English.FunctionWords.was : AuxEntry

Equations

• Fragments.English.FunctionWords.was = { form := "was", auxType := Fragments.English.FunctionWords.AuxType.be, number := some Number.sg, tense := some UD.Tense.Past, negForm := some "wasn't" }

def Fragments.English.FunctionWords.were : AuxEntry

Equations

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

def Fragments.English.FunctionWords.have_ : AuxEntry

Equations

• Fragments.English.FunctionWords.have_ = { form := "have", auxType := Fragments.English.FunctionWords.AuxType.have, number := some Number.pl, negForm := some "haven't" }

def Fragments.English.FunctionWords.has : AuxEntry

Equations

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

def Fragments.English.FunctionWords.had : AuxEntry

Equations

• Fragments.English.FunctionWords.had = { form := "had", auxType := Fragments.English.FunctionWords.AuxType.have, tense := some UD.Tense.Past, negForm := some "hadn't" }

def Fragments.English.FunctionWords.allAuxiliaries : List AuxEntry

Equations

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

def Fragments.English.FunctionWords.AuxEntry.toWord (a : AuxEntry) : Word

Equations

• a.toWord = { form := a.form, cat := UD.UPOS.AUX, features := { number := a.number, person := a.person } }

def Fragments.English.FunctionWords.AuxEntry.toModalItem (a : AuxEntry) : Core.Modality.ModalItem

Project to the shared modal item core (form + meaning + register).

Equations

• a.toModalItem = { form := a.form, meaning := a.modalMeaning, register := a.register }

structure Fragments.English.FunctionWords.ModalAdvEntry : Type

Modal adverb entry: an adverb expressing modal force and flavor without auxiliary morphology.

Modal adverbs participate in concord constructions where two modal expressions yield a single-modality reading.

• form : String
• modalMeaning : List Core.Modality.ForceFlavor

  Modal meaning in the force-flavor space.

• register : Core.Register.Level

  Register level.

def Fragments.English.FunctionWords.instReprModalAdvEntry.repr : ModalAdvEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.FunctionWords.instReprModalAdvEntry : Repr ModalAdvEntry

Equations

• Fragments.English.FunctionWords.instReprModalAdvEntry = { reprPrec := Fragments.English.FunctionWords.instReprModalAdvEntry.repr }

instance Fragments.English.FunctionWords.instBEqModalAdvEntry : BEq ModalAdvEntry

Equations

• Fragments.English.FunctionWords.instBEqModalAdvEntry = { beq := Fragments.English.FunctionWords.instBEqModalAdvEntry.beq }

def Fragments.English.FunctionWords.instBEqModalAdvEntry.beq : ModalAdvEntry → ModalAdvEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.FunctionWords.instBEqModalAdvEntry.beq x✝¹ x✝ = false

def Fragments.English.FunctionWords.ModalAdvEntry.toWord (a : ModalAdvEntry) : Word

Equations

• a.toWord = { form := a.form, cat := UD.UPOS.ADV }

def Fragments.English.FunctionWords.ModalAdvEntry.toModalItem (a : ModalAdvEntry) : Core.Modality.ModalItem

Project to the shared modal item core (form + meaning + register).

Equations

• a.toModalItem = { form := a.form, meaning := a.modalMeaning, register := a.register }

def Fragments.English.FunctionWords.certainly : ModalAdvEntry

Equations

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

def Fragments.English.FunctionWords.definitely : ModalAdvEntry

Equations

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

def Fragments.English.FunctionWords.necessarily : ModalAdvEntry

Equations

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

def Fragments.English.FunctionWords.possibly : ModalAdvEntry

Equations

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

def Fragments.English.FunctionWords.perhaps : ModalAdvEntry

Equations

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

def Fragments.English.FunctionWords.maybe : ModalAdvEntry

Equations

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

def Fragments.English.FunctionWords.probably : ModalAdvEntry

Equations

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

def Fragments.English.FunctionWords.potentially : ModalAdvEntry

Equations

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

def Fragments.English.FunctionWords.allModalAdverbs : List ModalAdvEntry

Equations

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

structure Fragments.English.FunctionWords.ConjEntry : Type

• form : String
• coordinating : Bool

  Coordinating or subordinating?

instance Fragments.English.FunctionWords.instReprConjEntry : Repr ConjEntry

Equations

• Fragments.English.FunctionWords.instReprConjEntry = { reprPrec := Fragments.English.FunctionWords.instReprConjEntry.repr }

def Fragments.English.FunctionWords.instReprConjEntry.repr : ConjEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.FunctionWords.instBEqConjEntry : BEq ConjEntry

Equations

• Fragments.English.FunctionWords.instBEqConjEntry = { beq := Fragments.English.FunctionWords.instBEqConjEntry.beq }

def Fragments.English.FunctionWords.instBEqConjEntry.beq : ConjEntry → ConjEntry → Bool

Equations

• Fragments.English.FunctionWords.instBEqConjEntry.beq { form := a, coordinating := a_1 } { form := b, coordinating := b_1 } = (a == b && a_1 == b_1)
• Fragments.English.FunctionWords.instBEqConjEntry.beq x✝¹ x✝ = false

def Fragments.English.FunctionWords.and_ : ConjEntry

Equations

• Fragments.English.FunctionWords.and_ = { form := "and" }

def Fragments.English.FunctionWords.or_ : ConjEntry

Equations

• Fragments.English.FunctionWords.or_ = { form := "or" }

def Fragments.English.FunctionWords.but : ConjEntry

Equations

• Fragments.English.FunctionWords.but = { form := "but" }

def Fragments.English.FunctionWords.nor : ConjEntry

Equations

• Fragments.English.FunctionWords.nor = { form := "nor" }

def Fragments.English.FunctionWords.allConjunctions : List ConjEntry

Equations

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

def Fragments.English.FunctionWords.ConjEntry.toWord (c : ConjEntry) : Word

Equations

• c.toWord = { form := c.form, cat := if c.coordinating = true then UD.UPOS.CCONJ else UD.UPOS.SCONJ }

structure Fragments.English.FunctionWords.ParticleEntry : Type

• form : String
• requiresSharedCQ : Bool

  Does this particle require the CQ to be commonly shared?

• nonRoothianAlts : Bool

  Can it access non-Roothian alternatives?

def Fragments.English.FunctionWords.instReprParticleEntry.repr : ParticleEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.FunctionWords.instReprParticleEntry : Repr ParticleEntry

Equations

• Fragments.English.FunctionWords.instReprParticleEntry = { reprPrec := Fragments.English.FunctionWords.instReprParticleEntry.repr }

def Fragments.English.FunctionWords.instBEqParticleEntry.beq : ParticleEntry → ParticleEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.FunctionWords.instBEqParticleEntry.beq x✝¹ x✝ = false

instance Fragments.English.FunctionWords.instBEqParticleEntry : BEq ParticleEntry

Equations

• Fragments.English.FunctionWords.instBEqParticleEntry = { beq := Fragments.English.FunctionWords.instBEqParticleEntry.beq }

def Fragments.English.FunctionWords.just_ : ParticleEntry

Equations

• Fragments.English.FunctionWords.just_ = { form := "just", requiresSharedCQ := false, nonRoothianAlts := true }

def Fragments.English.FunctionWords.only_ : ParticleEntry

Equations

• Fragments.English.FunctionWords.only_ = { form := "only", requiresSharedCQ := true, nonRoothianAlts := false }

def Fragments.English.FunctionWords.allParticles : List ParticleEntry

Equations

• Fragments.English.FunctionWords.allParticles = [Fragments.English.FunctionWords.just_, Fragments.English.FunctionWords.only_]

inductive Fragments.English.FunctionWords.AdvQuantForce : Type

Quantificational force for adverbial quantifiers.

• universal : AdvQuantForce
• existential : AdvQuantForce
• proportional : AdvQuantForce
• negative : AdvQuantForce

instance Fragments.English.FunctionWords.instDecidableEqAdvQuantForce : DecidableEq AdvQuantForce

Equations

• Fragments.English.FunctionWords.instDecidableEqAdvQuantForce x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.English.FunctionWords.instReprAdvQuantForce : Repr AdvQuantForce

Equations

• Fragments.English.FunctionWords.instReprAdvQuantForce = { reprPrec := Fragments.English.FunctionWords.instReprAdvQuantForce.repr }

def Fragments.English.FunctionWords.instReprAdvQuantForce.repr : AdvQuantForce → ℕ → Std.Format

Equations

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

instance Fragments.English.FunctionWords.instBEqAdvQuantForce : BEq AdvQuantForce

Equations

• Fragments.English.FunctionWords.instBEqAdvQuantForce = { beq := Fragments.English.FunctionWords.instBEqAdvQuantForce.beq }

def Fragments.English.FunctionWords.instBEqAdvQuantForce.beq : AdvQuantForce → AdvQuantForce → Bool

Equations

• Fragments.English.FunctionWords.instBEqAdvQuantForce.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Fragments.English.FunctionWords.AdvQuantEntry : Type

An adverbial quantifier entry: a closed-class adverb that quantifies over situations (times, events, occasions).

In @cite{percus-2000}'s framework, adverbial quantifiers take a situation pronoun that determines their domain and introduce a new λs binder over their nuclear scope. Generalization Y constrains the situation pronoun to be bound by the nearest c-commanding λ.

• form : String
• force : AdvQuantForce

  Quantificational force.

def Fragments.English.FunctionWords.instReprAdvQuantEntry.repr : AdvQuantEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.FunctionWords.instReprAdvQuantEntry : Repr AdvQuantEntry

Equations

• Fragments.English.FunctionWords.instReprAdvQuantEntry = { reprPrec := Fragments.English.FunctionWords.instReprAdvQuantEntry.repr }

def Fragments.English.FunctionWords.instBEqAdvQuantEntry.beq : AdvQuantEntry → AdvQuantEntry → Bool

Equations

• Fragments.English.FunctionWords.instBEqAdvQuantEntry.beq { form := a, force := a_1 } { form := b, force := b_1 } = (a == b && a_1 == b_1)
• Fragments.English.FunctionWords.instBEqAdvQuantEntry.beq x✝¹ x✝ = false

instance Fragments.English.FunctionWords.instBEqAdvQuantEntry : BEq AdvQuantEntry

Equations

• Fragments.English.FunctionWords.instBEqAdvQuantEntry = { beq := Fragments.English.FunctionWords.instBEqAdvQuantEntry.beq }

def Fragments.English.FunctionWords.always : AdvQuantEntry

Equations

• Fragments.English.FunctionWords.always = { form := "always", force := Fragments.English.FunctionWords.AdvQuantForce.universal }

def Fragments.English.FunctionWords.usually : AdvQuantEntry

Equations

• Fragments.English.FunctionWords.usually = { form := "usually", force := Fragments.English.FunctionWords.AdvQuantForce.proportional }

def Fragments.English.FunctionWords.sometimes : AdvQuantEntry

Equations

• Fragments.English.FunctionWords.sometimes = { form := "sometimes", force := Fragments.English.FunctionWords.AdvQuantForce.existential }

def Fragments.English.FunctionWords.never : AdvQuantEntry

Equations

• Fragments.English.FunctionWords.never = { form := "never", force := Fragments.English.FunctionWords.AdvQuantForce.negative }

def Fragments.English.FunctionWords.allAdvQuants : List AdvQuantEntry

Equations

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

def Fragments.English.FunctionWords.toInf : Word

Infinitival marker "to" (UD: PART). Distinct from the preposition "to" (ADP). Used in infinitival complements: "John managed to sleep".

Equations

• Fragments.English.FunctionWords.toInf = Word.mk' "to" UD.UPOS.PART