An indexical is a reactive functional rule of the form
X in R, where R is a set 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. When a propagating indexical fires, R is
evaluated in the current store S, which is extended by adding the
new domain constraint X::S(R) to the store, where
S(R) denotes the value of R in S. When a checking
indexical fires, it checks if D(X,S) is contained in S(R),
and if so, the constraint corresponding to the indexical is detected as
entailed.