Point temporal relations

The point analogue of AllenRelation (which operates on intervals). A Relation is a domain-flavored selector over the standard partition of pairs of times: before, after, overlapping, ≤, ≥, unrestricted.

Used by tense (past/present/future via Core.Time.Tense.GramTense.toRelation), evidential semantics (EPCondition.toRelation), and modal-base time analyses (MBTProfile.toRelation in Huijsmans 2025) — each domain provides a name for one shape from the same partition.

inductive Core.Time.Relation : Type

Temporal relation type for tense operators. Relates two times (typically event time and reference/speech time). The point analogue of AllenRelation (which operates on intervals).

• before : Relation
• after : Relation
• overlapping : Relation
• notAfter : Relation
• notBefore : Relation
• unrestricted : Relation

@[implicit_reducible]

instance Core.Time.instDecidableEqRelation : DecidableEq Relation

Equations

• Core.Time.instDecidableEqRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Time.instReprRelation.repr : Relation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.Time.instReprRelation.repr Core.Time.Relation.before prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Time.Relation.before")).group prec✝
• Core.Time.instReprRelation.repr Core.Time.Relation.after prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Time.Relation.after")).group prec✝

@[implicit_reducible]

instance Core.Time.instReprRelation : Repr Relation

Equations

• Core.Time.instReprRelation = { reprPrec := Core.Time.instReprRelation.repr }

def Core.Time.Relation.eval {Time : Type u_1} [LinearOrder Time] : Relation → Time → Time → Prop

Evaluate a temporal relation on two times

Equations

• Core.Time.Relation.before.eval x✝¹ x✝ = (x✝¹ < x✝)
• Core.Time.Relation.after.eval x✝¹ x✝ = (x✝¹ > x✝)
• Core.Time.Relation.overlapping.eval x✝¹ x✝ = (x✝¹ = x✝)
• Core.Time.Relation.notAfter.eval x✝¹ x✝ = (x✝¹ ≤ x✝)
• Core.Time.Relation.notBefore.eval x✝¹ x✝ = (x✝¹ ≥ x✝)
• Core.Time.Relation.unrestricted.eval x✝¹ x✝ = True

@[implicit_reducible]

instance Core.Time.Relation.instDecidableEvalOfDecidableEq {Time : Type u_1} [LinearOrder Time] [DecidableEq Time] (r : Relation) (t₁ t₂ : Time) : Decidable (r.eval t₁ t₂)

Equations

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