cv_trans : thm -> unit
STRUCTURE
cv_transLib
SYNOPSIS
Translates functional definitions to the cv_compute subset of HOL.
LIBRARY
cv_transLib
DESCRIPTION
This function is the same as cv_transLib.cv_trans_pre, except that it tries to discharge any preconditions automatically.
FAILURE
When translation produces a precondition that cv_transLib.cv_trans cannot prove automatically, or encounters a sub-term containing a constant that has not already been translated, or cv_transLib.cv_termination_tac fails to prove the termination goal of the translator-defined :cv function. In the latter case, the termination goal is pushed onto the goal stack.
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
COMMENTS
Designed to produce definitions suitable for evaluation by cv_transLib.cv_eval.
SEEALSO
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, cv_termination_tac
HOL  Trindemossen-1