deep_alpha : (string * string) list -> term -> term
Modify bound variable according to renaming scheme.
When applied to a list of string-string pairs
a conversion results that will attempt to traverse a term and
systematically replace any bound variable called xi with one called xi'. It
will quietly do nothing in cases where that is impossible because of variable
deep_alpha ["x1'","x1"; ...; "xn'","xn"]
# deep_alpha ["x'","x"; "y'","y"] `?x. x <=> !y. y = y`;;
Warning: inventing type variables
val it : term = `?x'. x' <=> (!y'. y' = y')`
This is used inside PART_MATCH to try to achieve a reasonable correspondence
in bound variable names, e.g. so that the bound variable is still called `n'
rather than `x' here:
# REWR_CONV NOT_FORALL_THM `~(!n. n < m)`;;
val it : thm = |- ~(!n. n < m) <=> (?n. ~(n < m))
- SEE ALSO