Indices of evaluation

An index of evaluation is a world–time pair, the circumstance of evaluation of [kaplan-1989] with world and temporal coordinates only: a product, with its coordinates named (Index.world, Index.time), so that the Prod instances and API apply. It is not the Kratzer situation, a preordered type with parthood, nor the Pearl–Halpern partial valuation (Causation.Situation).

References

• [kaplan-1989]

@[reducible, inline]

abbrev Reference.Index (W : Type u_1) (T : Type u_2) : Type (max u_1 u_2)

A world–time index of evaluation.

Equations

• Reference.Index W T = (W × T)

@[reducible, inline]

abbrev Reference.Index.world {W : Type u_1} {T : Type u_2} (i : Index W T) : W

The world coordinate.

Equations

• i.world = i.fst

@[reducible, inline]

abbrev Reference.Index.time {W : Type u_1} {T : Type u_2} (i : Index W T) : T

The temporal coordinate.

Equations

• i.time = i.snd

@[simp]

theorem Reference.Index.world_mk {W : Type u_1} {T : Type u_2} (w : W) (t : T) : world (w, t) = w

@[simp]

theorem Reference.Index.time_mk {W : Type u_1} {T : Type u_2} (w : W) (t : T) : time (w, t) = t