inductive Fragments.English.TemporalAdverbials.AdverbialPosition : Type

Syntactic position of a temporal adverbial. @cite{rouillard-2026} schemata (57), (61):

• eventLevel: modifies VP (E-TIA reading)
• perfectLevel: modifies AspP (G-TIA reading)

• eventLevel : AdverbialPosition
• perfectLevel : AdverbialPosition

instance Fragments.English.TemporalAdverbials.instDecidableEqAdverbialPosition : DecidableEq AdverbialPosition

Equations

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

instance Fragments.English.TemporalAdverbials.instBEqAdverbialPosition : BEq AdverbialPosition

Equations

• Fragments.English.TemporalAdverbials.instBEqAdverbialPosition = { beq := Fragments.English.TemporalAdverbials.instBEqAdverbialPosition.beq }

def Fragments.English.TemporalAdverbials.instBEqAdverbialPosition.beq : AdverbialPosition → AdverbialPosition → Bool

Equations

• Fragments.English.TemporalAdverbials.instBEqAdverbialPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.TemporalAdverbials.instReprAdverbialPosition : Repr AdverbialPosition

Equations

• Fragments.English.TemporalAdverbials.instReprAdverbialPosition = { reprPrec := Fragments.English.TemporalAdverbials.instReprAdverbialPosition.repr }

def Fragments.English.TemporalAdverbials.instReprAdverbialPosition.repr : AdverbialPosition → ℕ → Std.Format

Equations

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

inductive Fragments.English.TemporalAdverbials.MapFunction : Type

Map function type: what does in relate to time? @cite{rouillard-2026} eqs. (62)--(64), (70):

• runtime: M = τ (temporal trace); used for E-TIAs
• identity: M = id; used for G-TIAs (times map to themselves)

• runtime : MapFunction
• identity : MapFunction

instance Fragments.English.TemporalAdverbials.instDecidableEqMapFunction : DecidableEq MapFunction

Equations

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

instance Fragments.English.TemporalAdverbials.instBEqMapFunction : BEq MapFunction

Equations

• Fragments.English.TemporalAdverbials.instBEqMapFunction = { beq := Fragments.English.TemporalAdverbials.instBEqMapFunction.beq }

def Fragments.English.TemporalAdverbials.instBEqMapFunction.beq : MapFunction → MapFunction → Bool

Equations

• Fragments.English.TemporalAdverbials.instBEqMapFunction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.TemporalAdverbials.instReprMapFunction : Repr MapFunction

Equations

• Fragments.English.TemporalAdverbials.instReprMapFunction = { reprPrec := Fragments.English.TemporalAdverbials.instReprMapFunction.repr }

def Fragments.English.TemporalAdverbials.instReprMapFunction.repr : MapFunction → ℕ → Std.Format

Equations

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

inductive Fragments.English.TemporalAdverbials.TIAType : Type

Temporal adverbial type. @cite{rouillard-2026} terminology.

• eTIA : TIAType
• gTIA : TIAType

instance Fragments.English.TemporalAdverbials.instDecidableEqTIAType : DecidableEq TIAType

Equations

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

instance Fragments.English.TemporalAdverbials.instBEqTIAType : BEq TIAType

Equations

• Fragments.English.TemporalAdverbials.instBEqTIAType = { beq := Fragments.English.TemporalAdverbials.instBEqTIAType.beq }

def Fragments.English.TemporalAdverbials.instBEqTIAType.beq : TIAType → TIAType → Bool

Equations

• Fragments.English.TemporalAdverbials.instBEqTIAType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.TemporalAdverbials.instReprTIAType : Repr TIAType

Equations

• Fragments.English.TemporalAdverbials.instReprTIAType = { reprPrec := Fragments.English.TemporalAdverbials.instReprTIAType.repr }

def Fragments.English.TemporalAdverbials.instReprTIAType.repr : TIAType → ℕ → Std.Format

Equations

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

inductive Fragments.English.TemporalAdverbials.AspectReq : Type

Aspect required by the adverbial's LF (E-perfect vs U-perfect). @cite{rouillard-2026} Table 1.

• perfective : AspectReq
• imperfective : AspectReq
• either : AspectReq

instance Fragments.English.TemporalAdverbials.instDecidableEqAspectReq : DecidableEq AspectReq

Equations

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

instance Fragments.English.TemporalAdverbials.instBEqAspectReq : BEq AspectReq

Equations

• Fragments.English.TemporalAdverbials.instBEqAspectReq = { beq := Fragments.English.TemporalAdverbials.instBEqAspectReq.beq }

def Fragments.English.TemporalAdverbials.instBEqAspectReq.beq : AspectReq → AspectReq → Bool

Equations

• Fragments.English.TemporalAdverbials.instBEqAspectReq.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.English.TemporalAdverbials.instReprAspectReq.repr : AspectReq → ℕ → Std.Format

Equations

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

instance Fragments.English.TemporalAdverbials.instReprAspectReq : Repr AspectReq

Equations

• Fragments.English.TemporalAdverbials.instReprAspectReq = { reprPrec := Fragments.English.TemporalAdverbials.instReprAspectReq.repr }

structure Fragments.English.TemporalAdverbials.TIAEntry : Type

A lexical entry for a temporal in-adverbial or related adverbial. Theory-typed but theory-neutral: records structural properties without committing to a specific analysis of the perfect or aspect.

• preposition : String

  Surface preposition

• tiaType : TIAType

  TIA type

• position : AdverbialPosition

  Syntactic position

• mapFunction : MapFunction

  Map function

• requiresTelic : Bool

  Requires telic VP? (for E-TIAs)

• requiresNegative : Bool

  Requires negative polarity? (for G-TIAs)

• requiresPerfect : Bool

  Requires the perfect?

• aspectReq : AspectReq

  Aspectual requirement

• isNPI : Bool

  Is this an NPI?

def Fragments.English.TemporalAdverbials.instReprTIAEntry.repr : TIAEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.TemporalAdverbials.instReprTIAEntry : Repr TIAEntry

Equations

• Fragments.English.TemporalAdverbials.instReprTIAEntry = { reprPrec := Fragments.English.TemporalAdverbials.instReprTIAEntry.repr }

def Fragments.English.TemporalAdverbials.instBEqTIAEntry.beq : TIAEntry → TIAEntry → Bool

Equations

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

instance Fragments.English.TemporalAdverbials.instBEqTIAEntry : BEq TIAEntry

Equations

• Fragments.English.TemporalAdverbials.instBEqTIAEntry = { beq := Fragments.English.TemporalAdverbials.instBEqTIAEntry.beq }

def Fragments.English.TemporalAdverbials.inETIA : TIAEntry

in as E-TIA: "wrote a paper in three days". @cite{rouillard-2026} eq. (62): ⟦in⟧ := λM λt λx. M(x) ⊑ t. Position: event-level (VP-adjacent). Map function: τ (runtime). Licensed when VP is telic. Not an NPI.

Equations

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

def Fragments.English.TemporalAdverbials.inGTIA : TIAEntry

in as G-TIA: "hasn't been sick in three days". @cite{rouillard-2026} eq. (70): ⟦id⟧ := id. Position: perfect-level (AspP-adjacent). Map function: id (times map to themselves). Licensed only under negation in the perfect. NPI.

Equations

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

inductive Fragments.English.TemporalAdverbials.TemporalAdvType : Type

Temporal adverbial type for non-TIA temporal expressions.

• since_ : TemporalAdvType
• for_ : TemporalAdvType
• ago : TemporalAdvType
• before_ : TemporalAdvType

instance Fragments.English.TemporalAdverbials.instDecidableEqTemporalAdvType : DecidableEq TemporalAdvType

Equations

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

instance Fragments.English.TemporalAdverbials.instBEqTemporalAdvType : BEq TemporalAdvType

Equations

• Fragments.English.TemporalAdverbials.instBEqTemporalAdvType = { beq := Fragments.English.TemporalAdverbials.instBEqTemporalAdvType.beq }

def Fragments.English.TemporalAdverbials.instBEqTemporalAdvType.beq : TemporalAdvType → TemporalAdvType → Bool

Equations

• Fragments.English.TemporalAdverbials.instBEqTemporalAdvType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.TemporalAdverbials.instReprTemporalAdvType : Repr TemporalAdvType

Equations

• Fragments.English.TemporalAdverbials.instReprTemporalAdvType = { reprPrec := Fragments.English.TemporalAdverbials.instReprTemporalAdvType.repr }

def Fragments.English.TemporalAdverbials.instReprTemporalAdvType.repr : TemporalAdvType → ℕ → Std.Format

Equations

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

structure Fragments.English.TemporalAdverbials.TemporalAdvEntry : Type

A non-TIA temporal adverbial entry.

• form : String

  Surface form

• advType : TemporalAdvType

  Adverbial type

• specifiesLB : Bool

  Specifies LB of PTS? (@cite{iatridou-anagnostopoulou-izvorski-2001} classification)

• requiresPerfect : Bool

  Requires the perfect?

• perfectAmbiguity : Bool

  Is ambiguous between E- and U-perfect?

def Fragments.English.TemporalAdverbials.instReprTemporalAdvEntry.repr : TemporalAdvEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.TemporalAdverbials.instReprTemporalAdvEntry : Repr TemporalAdvEntry

Equations

• Fragments.English.TemporalAdverbials.instReprTemporalAdvEntry = { reprPrec := Fragments.English.TemporalAdverbials.instReprTemporalAdvEntry.repr }

def Fragments.English.TemporalAdverbials.instBEqTemporalAdvEntry.beq : TemporalAdvEntry → TemporalAdvEntry → Bool

Equations

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

instance Fragments.English.TemporalAdverbials.instBEqTemporalAdvEntry : BEq TemporalAdvEntry

Equations

• Fragments.English.TemporalAdverbials.instBEqTemporalAdvEntry = { beq := Fragments.English.TemporalAdverbials.instBEqTemporalAdvEntry.beq }

def Fragments.English.TemporalAdverbials.since : TemporalAdvEntry

"since Monday": left-bounds the PTS. Durative adverbial: specifies LB. @cite{von-fintel-iatridou-2019}: not lexically ambiguous.

Equations

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

def Fragments.English.TemporalAdverbials.forAdv : TemporalAdvEntry

"for three days": event-level duration. Ambiguous between event-level (measures event) and perfect-level (measures PTS). @cite{rouillard-2026} fn. 10.

Equations

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

def Fragments.English.TemporalAdverbials.ago : TemporalAdvEntry

"three days ago": simple past reference.

Equations

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

def Fragments.English.TemporalAdverbials.TIAEntry.isEventLevel (e : TIAEntry) : Bool

E-TIA vs G-TIA is determined by syntactic position. @cite{rouillard-2026} schemata (61): (a) ASP [ VP E-TIA] (b) [ ASP VP] G-TIA

Equations

• e.isEventLevel = (e.position == Fragments.English.TemporalAdverbials.AdverbialPosition.eventLevel)

def Fragments.English.TemporalAdverbials.TIAEntry.usesRuntime (e : TIAEntry) : Bool

Does this TIA type use the runtime function τ?

Equations

• e.usesRuntime = (e.mapFunction == Fragments.English.TemporalAdverbials.MapFunction.runtime)

def Fragments.English.TemporalAdverbials.TIAEntry.vendlerConstraint (e : TIAEntry) : Option Semantics.Tense.Aspect.LexicalAspect.Telicity

The Vendler class constraint for E-TIAs: telic VPs only.

Equations

• e.vendlerConstraint = if e.requiresTelic = true then some Semantics.Tense.Aspect.LexicalAspect.Telicity.telic else none

def Fragments.English.TemporalAdverbials.allTIAs : List TIAEntry

All TIA entries (both readings of in).

Equations

• Fragments.English.TemporalAdverbials.allTIAs = [Fragments.English.TemporalAdverbials.inETIA, Fragments.English.TemporalAdverbials.inGTIA]

def Fragments.English.TemporalAdverbials.allTemporalAdvs : List TemporalAdvEntry

All temporal adverbial entries.

Equations

• Fragments.English.TemporalAdverbials.allTemporalAdvs = [Fragments.English.TemporalAdverbials.since, Fragments.English.TemporalAdverbials.forAdv, Fragments.English.TemporalAdverbials.ago]