Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

SPEC_TAC : term * term -> tactic

SYNOPSIS

Generalizes a goal.

DESCRIPTION

When applied to a pair of terms (`u`,`x`), where x is just a variable, and a goal A ?- t, the tactic SPEC_TAC generalizes the goal to A ?- !x. t[x/u], that is, all (free) instances of u are turned into x.

        A ?- t
   =================  SPEC_TAC (`u`,`x`)
    A ?- !x. t[x/u]

FAILURE CONDITIONS

Fails unless x is a variable with the same type as u.

USES

Removing unnecessary speciality in a goal, particularly as a prelude to an inductive proof.