FILTER_PGEN_TAC

PairRules.FILTER_PGEN_TAC : (term -> tactic)

Strips off a paired universal quantifier, but fails for a given quantified pair.

When applied to a term q and a goal A ?- !p. t, the tactic FILTER_PGEN_TAC fails if the quantified pair p is the same as p, but otherwise advances the goal in the same way as PGEN_TAC, i.e. returns the goal A ?- t[p'/p] where p' is a variant of p chosen to avoid clashing with any variables free in the goal’s assumption list. Normally p' is just p.

     A ?- !p. t
   ==============  FILTER_PGEN_TAC "q"
    A ?- t[p'/p]

Failure

Fails if the goal’s conclusion is not a paired universal quantifier or the quantified pair is equal to the given term.

See also

Tactic.FILTER_GEN_TAC, PairRules.PGEN, PairRules.PGEN_TAC, PairRules.PGENL, PairRules.PSPEC, PairRules.PSPECL, PairRules.PSPEC_ALL, PairRules.PSPEC_TAC, PairRules.PSTRIP_TAC