cv_eval : term -> thm
STRUCTURE
cv_transLib
SYNOPSIS
Uses cv_computeLib to evaluate closed terms, equipped with translations from cv_transLib.
LIBRARY
cv_transLib
DESCRIPTION
Provides a user-friendly interface to cv_computeLib.cv_compute, as long as cv_transLib has been used to translate all constants in the given input term.
FAILURE
When the input term contains either free variables or constants which have not yet been translated.
EXAMPLE
> cv_trans arithmeticTheory.FACT;
Equations stored under "cv_FACT_def".
Induction stored under "cv_FACT_ind".
Finished translating FACT, stored in cv_FACT_thm
val it = (): unit
> cv_eval “FACT 50”;
val it =
   ⊢ FACT 50 =
     30414093201713378043612608166064768844377641568960512000000000000: thm
SEEALSO
cv_trans, cv_trans_pre, cv_trans_pre_rec, cv_trans_rec, cv_auto_trans, cv_auto_trans_pre, cv_auto_trans_pre_rec, cv_auto_trans_rec, cv_eval_raw, cv_termination_tac
HOL  Trindemossen-1