Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-11 17:41:45 -0800 (Fri, 11 Mar 2005)
Revision: 6907
Log message:
In a rewriter, I added a way to consider "!v" as bindings. If a term
Perv!xbinder{!v} is specified as one of the rewrite arguments, then 'v is
considered "bound" in the redex. In other words, terms like 'e[!v] in the
redex would be considered _patterns_ for 'e (so no need to pass in
bind{x.'e['x]} any more).
Note that while the implementation of such a rule will now require that all
the occurrence of !v in 'e are "selected", we should still consider the
semantics to be the original one (where any subset of !v occurrences might get
"selected"). Otherwise we might get into trouble with derived rules/rewrite
(I am not sure).