cv_auto_trans_pre_rec

cv_transLib.cv_auto_trans_pre_rec : string -> thm -> tactic -> thm

Translates functional definitions to the cv_compute subset of HOL.

This is a recursive version of cv_transLib.cv_trans_pre_rec. During translation of the given HOL function, cv_transLib.cv_auto_trans_pre_rec will call itself recursively on the definitions of any not-yet-translated constants it encounters.

As with all auto variants, cv_transLib.cv_auto_trans_pre_rec can sometimes translate uses of higher-order functions, such as MAP.

Failure

When the translation produces a precondition that cv_transLib.cv_auto_trans_pre_rec cannot prove automatically, or cv_transLib.cv_termination_tac fails to prove the termination goal of any recursively translated function, or the provided tactic fails to prove the termination goal of the top-level translator-defined :cv function.

Example

See cv_transLib.cv_auto_trans and cv_transLib.cv_trans_pre_rec for relevant examples.

Comments

Designed to produce definitions suitable for evaluation by cv_transLib.cv_eval.

See also

cv_transLib.cv_trans, cv_transLib.cv_trans_pre, cv_transLib.cv_trans_pre_rec, cv_transLib.cv_trans_rec, cv_transLib.cv_auto_trans, cv_transLib.cv_auto_trans_pre, cv_transLib.cv_auto_trans_rec, cv_transLib.cv_eval, cv_transLib.cv_termination_tac