X_GEN_TAC : term -> tactic

SYNOPSIS

Specializes a goal with the given variable.

DESCRIPTION

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.

USES

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.