Applies a term-tactic to a goal’s “first” free variable
DESCRIPTION
Applying fv_term tmtac to a goal A ?- g, finds the first free
variable in the goal, and passes that variable to the function
tmtac, generating a tactic, which is then applied to the goal. The
first free variable is the first returned by successive calls to
free_vars applied to first g and then each assumption in A in
turn.
FAILURE
Fails if a goal does not have any free variables, or if tmtac v
fails when applied to the goal, with v the “first” free variable
as defined above.
EXAMPLE
?- 0 < f (n:num)
================================== fv_term (C tmCases_on ["", "j"])
?- 0 < f 0 ?- 0 < f (SUC j)