EVAL_TAC : tactic
STRUCTURE
bossLib
SYNOPSIS
Evaluate a goal deductively.
DESCRIPTION
Applying EVAL_TAC to a goal A ?- g results in EVAL being applied to g to obtain |- g = g'. This theorem is used to transform the goal to A ?- g'.

The notion of evaluation is based around rules for replacing constants by their (equational) definitions. Thus EVAL_TAC is currently suited to evaluation of expressions that look like functional programs. Evaluation of inductive relations is not currently supported.

FAILURE
Shouldn’t fail, but may diverge.
EXAMPLE
EVAL_TAC reduces the goal ?-  P (REVERSE (FLAT [[x; y]; [a; b; c; d]])) to the goal 
   ?- P [d; c; b; a; y; x]
COMMENTS
The main problem with EVAL_TAC is knowing when it will terminate. One typical cause of non-termination is that a constant in the goal has not been added to the_compset. Another is that a test in a conditional in the expression may involve a variable.
USES
Symbolic evaluation.
SEEALSO
EVAL
HOL  Kananaskis-14