pvariant
PairRules.pvariant : (term list -> term -> term)
Modifies variable and constant names in a paired structure to avoid clashes.
When applied to a list of (possibly paired structures of) variables to
avoid clashing with, and a pair to modify, pvariant returns a variant
of the pair. That is, it changes the names of variables and constants in
the pair as intuitively as possible to make them distinct from any
variables in the list, or any (non-hidden) constants. This is normally
done by adding primes to the names.
The exact form of the altered names should not be relied on, except that the original variables will be unmodified unless they are in the list to avoid clashing with. Also note that if the same variable occurs more that one in the pair, then each instance of the variable will be modified in the same way.
Failure
pvariant l p fails if any term in the list l is not a paired
structure of variables, or if p is not a paired structure of variables
and constants.
Example
The following shows a case that exhibits most possible behaviours:
- pvariant [Term `b:'a`, Term `(c:'a,c':'a)`]
(Term `((a:'a,b:'a),(c:'a,b':'a,T,b:'a))`);
val it = `(a,b''),c'',b',T',b''` : term
The function pvariant is extremely useful for complicated derived
rules which need to rename pairs variable to avoid free variable capture
while still making the role of the pair obvious to the user.