deep_alpha : (string * string) list -> term -> term

SYNOPSIS

Modify bound variable according to renaming scheme.

DESCRIPTION

When applied to a list of string-string pairs

  deep_alpha ["x1'","x1"; ...; "xn'","xn"]

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 capture.

EXAMPLE

  # deep_alpha ["x'","x"; "y'","y"] `?x. x <=> !y. y = y`;;
  Warning: inventing type variables
  val it : term = `?x'. x' <=> (!y'. y' = y')`

COMMENTS

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

alpha, PART_MATCH.