		Search-engine friendly clone of the ACL2 documentation.

Vl-translation-p

Vl-translation-get-esim

Get an E Module for a successfully translated module.

Signature
(vl-translation-get-esim modname x) → e-mod
Arguments: modname — Guard (stringp modname).; x — Guard (vl-translation-p x).

Definitions and Theorems

Function: vl-translation-get-esim

(defun vl-translation-get-esim (modname x)
 (declare (xargs :guard (and (stringp modname)
                             (vl-translation-p x))))
 (declare (xargs :guard (vl-translation-has-module modname x)))
 (let ((__function__ 'vl-translation-get-esim))
  (declare (ignorable __function__))
  (b*
   ((mod
        (vl-find-module modname
                        (vl-design->mods (vl-translation->good x))))
    (esim (vl-module->esim mod))
    ((unless esim)
     (raise "Module ~x0 has no esim?" modname)))
   esim)))