cv_eval_raw

cv_transLib.cv_eval_raw : term -> thm

Uses cv_computeLib to evaluate closed terms, equipped with translations from cv_transLib.

Like cv_transLib.cv_eval, except it omits the potentially expensive evaluation out of the :cv type.

Failure

Fails in the same ways as cv_transLib.cv_eval.

Example

> cv_transLib.cv_trans rich_listTheory.REPLICATE;
Finished translating REPLICATE, stored in cv_REPLICATE_thm
val it = (): unit
> cv_transLib.cv_eval “REPLICATE 3 (3:num)”;
val it = ⊢ REPLICATE 3 3 = [3; 3; 3]: thm
> cv_transLib.cv_eval_raw “REPLICATE 3 (3:num)”;
val it =
   ⊢ REPLICATE 3 3 =
     cv_type$to_list cv$c2n
       (cv$Pair (cv$Num 3)
          (cv$Pair (cv$Num 3) (cv$Pair (cv$Num 3) (cv$Num 0)))): thm

See also

cv_transLib.cv_eval