An indexical is a reactive functional rule of the form
`X`` in `

`R`, where `R` is a finite domain valued range
expression (see below). See Syntax of Indexicals for a grammar
defining indexicals and range expressions.

Indexicals can play one of two roles: propagating indexicals are
used for constraint solving, and checking indexicals are used for
entailment checking.
Let `S(R)` denote the value of `R` in `S`.
When a propagating indexical fires, the current store `S` is
extended to `(X in S(R))(S)`. When a checking indexical fires, it
checks if `D(X,S)` is contained in `S(R)`, in which case the
constraint corresponding to the indexical is detected as entailed.

Send feedback on this subject.