#### 34.9.1 Indexicals

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.