X_GEN_TAC : term -> tactic
Specializes a goal with the given variable.
When applied to a term x', which should be a variable, and a goal
A ?- !x. t, the tactic X_GEN_TAC returns the goal A ?- t[x'/x].
A ?- !x. t
============== X_GEN_TAC `x'`
A ?- t[x'/x]
- FAILURE CONDITIONS
Fails unless the goal's conclusion is universally quantified and the term a
variable of the appropriate type. It also fails if the variable given is free
in either the assumptions or (initial) conclusion of the goal.
It is perhaps good practice to use this rather than GEN_TAC, to ensure that
there is no dependency on the bound variable name in the goal, which can
sometimes arise somewhat arbitrarily, e.g. in higher-order matching.
- SEE ALSO
FIX_TAC, GEN, GENL, GEN_ALL, GEN_TAC, INTRO_TAC, SPEC, SPECL, SPEC_ALL,