Indices of evaluation

An Intensional.Index is a (world, time) pair used as a context of evaluation for intensional, dynamic, modal, and tense semantics — the Lewis/Kaplan "index of evaluation", with world and temporal coordinates only. It is not the full Kratzer parthood-structured situation (Intensional.Situations) and not the Pearl/Halpern partial valuation (Causation.Situation).

structure Intensional.Index (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 Intensional.Situations).

• world : W

  The world coordinate

• time : Time

  The temporal coordinate

@[instance_reducible]

instance Intensional.instReprIndex {W✝ : Type u_1} {Time✝ : Type u_2} [Repr W✝] [Repr Time✝] : Repr (Index W✝ Time✝)

Equations

• Intensional.instReprIndex = { reprPrec := Intensional.instReprIndex.repr }

def Intensional.instReprIndex.repr {W✝ : Type u_1} {Time✝ : Type u_2} [Repr W✝] [Repr Time✝] : Index W✝ Time✝ → Nat → Std.Format

Equations

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