World–Time Indices

A WorldTimeIndex is a (world, time) pair used as a context of evaluation for intensional, dynamic, modal, and tense semantics. This is the Lewis/Kaplan-style "index of evaluation" with world and temporal coordinates only — not the full Kratzer parthood-structured situation (see Core.Logic.Intensional.Situations) and not the Pearl/Halpern partial valuation (see Core.Causal.Situation).

The name WorldTimeIndex is preferred over Situation to disambiguate from the two more substantive Situation types in those neighbouring namespaces.

structure Core.WorldTimeIndex (W : Type u_1) (Time : Type u_2) : Type (max u_1 u_2)

A world–time index: a (world, time) pair used as a context of evaluation in intensional, dynamic, modal, and tense semantics.

This is the Lewis/Kaplan "index" — a coordinate tuple as point of evaluation, abstracting from the spatial/parthood structure of true Kratzer situations (see Core.Logic.Intensional.Situations).

• world : W

  The world coordinate

• time : Time

  The temporal coordinate

@[implicit_reducible]

instance Core.instReprWorldTimeIndex {W✝ : Type u_1} {Time✝ : Type u_2} [Repr W✝] [Repr Time✝] : Repr (WorldTimeIndex W✝ Time✝)

Equations

• Core.instReprWorldTimeIndex = { reprPrec := Core.instReprWorldTimeIndex.repr }

def Core.instReprWorldTimeIndex.repr {W✝ : Type u_1} {Time✝ : Type u_2} [Repr W✝] [Repr Time✝] : WorldTimeIndex W✝ Time✝ → Nat → Std.Format

Equations

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