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.