English Miscellaneous Function Words Fragment

Closed-class items that don't fit a more specific Fragment file:

• Prepositions (to_, on, in_, at_, by_, with_, from_, before, after)
• Coordinating conjunctions (and_, or_, but, nor)
• Adverbial quantifiers ([Per00]) — always, usually, sometimes, never

The auxiliaries (modals + do-support + be + have + modal adverbs + infinitival particle) live in Fragments/English/Auxiliaries.lean. The complementizers (that, if, whether, ...) live in Fragments/English/Complementizers.lean.

This file may be split further as topic-specific Fragment files emerge.

structure English.FunctionWords.PrepEntry : Type

• form : String
• passiveAgent : Bool

  Can introduce an agent in passive?

@[implicit_reducible]

instance English.FunctionWords.instReprPrepEntry : Repr PrepEntry

Equations

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

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

Equations

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

@[implicit_reducible]

instance English.FunctionWords.instBEqPrepEntry : BEq PrepEntry

Equations

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

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

Equations

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

def English.FunctionWords.to_ : PrepEntry

Equations

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

def English.FunctionWords.on : PrepEntry

Equations

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

def English.FunctionWords.in_ : PrepEntry

Equations

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

def English.FunctionWords.at_ : PrepEntry

Equations

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

def English.FunctionWords.by_ : PrepEntry

Equations

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

def English.FunctionWords.with_ : PrepEntry

Equations

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

def English.FunctionWords.from_ : PrepEntry

Equations

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

def English.FunctionWords.before : PrepEntry

Equations

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

def English.FunctionWords.after : PrepEntry

Equations

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

def English.FunctionWords.allPrepositions : List PrepEntry

Equations

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

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

Equations

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

structure English.FunctionWords.ConjEntry : Type

• form : String
• coordinating : Bool

  Coordinating or subordinating?

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

Equations

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

@[implicit_reducible]

instance English.FunctionWords.instReprConjEntry : Repr ConjEntry

Equations

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

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

Equations

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

@[implicit_reducible]

instance English.FunctionWords.instBEqConjEntry : BEq ConjEntry

Equations

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

def English.FunctionWords.and_ : ConjEntry

Equations

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

def English.FunctionWords.or_ : ConjEntry

Equations

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

def English.FunctionWords.but : ConjEntry

Equations

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

def English.FunctionWords.nor : ConjEntry

Equations

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

def English.FunctionWords.allConjunctions : List ConjEntry

Equations

• English.FunctionWords.allConjunctions = [English.FunctionWords.and_, English.FunctionWords.or_, English.FunctionWords.but, English.FunctionWords.nor]

def 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 }

inductive English.FunctionWords.AdvQuantForce : Type

Quantificational force for adverbial quantifiers.

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

@[implicit_reducible]

instance English.FunctionWords.instDecidableEqAdvQuantForce : DecidableEq AdvQuantForce

Equations

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

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

Equations

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

@[implicit_reducible]

instance English.FunctionWords.instReprAdvQuantForce : Repr AdvQuantForce

Equations

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

structure English.FunctionWords.AdvQuantEntry : Type

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

In [Per00]'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.

@[implicit_reducible]

instance English.FunctionWords.instReprAdvQuantEntry : Repr AdvQuantEntry

Equations

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

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

Equations

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

@[implicit_reducible]

instance English.FunctionWords.instBEqAdvQuantEntry : BEq AdvQuantEntry

Equations

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

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

Equations

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

def English.FunctionWords.always : AdvQuantEntry

Equations

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

def English.FunctionWords.usually : AdvQuantEntry

Equations

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

def English.FunctionWords.sometimes : AdvQuantEntry

Equations

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

def English.FunctionWords.never : AdvQuantEntry

Equations

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

def English.FunctionWords.allAdvQuants : List AdvQuantEntry

Equations

• English.FunctionWords.allAdvQuants = [English.FunctionWords.always, English.FunctionWords.usually, English.FunctionWords.sometimes, English.FunctionWords.never]