		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

Svexlists->a4vec-top

Signature
(svexlists->a4vec-top x y env masks) → (mv * *)
Arguments: x — Guard (svexlist-p x).; y — Guard (svexlist-p y).; env — Guard (svex-a4vec-env-p env).; masks — Guard (svex-mask-alist-p masks).

Definitions and Theorems

Function: svexlists->a4vec-top

(defun svexlists->a4vec-top (x y env masks)
 (declare (xargs :guard (and (svexlist-p x)
                             (svexlist-p y)
                             (svex-a4vec-env-p env)
                             (svex-mask-alist-p masks))))
 (let ((__function__ 'svexlists->a4vec-top))
  (declare (ignorable __function__))
  (mbe
   :logic
   (mv (svexlist->a4vec x env masks)
       (svexlist->a4vec y env masks))
   :exec
   (b*
    (((mv x-res y-res memo)
      (with-local-stobj
        acl2::nrev
        (mv-let
           (x-res y-res memo acl2::nrev)
           (b* (((mv acl2::nrev memo)
                 (svexlist->a4vec-nrev x env masks nil acl2::nrev))
                ((mv x-res acl2::nrev)
                 (acl2::nrev-finish acl2::nrev))
                ((mv acl2::nrev memo)
                 (svexlist->a4vec-nrev y env masks memo acl2::nrev))
                ((mv y-res acl2::nrev)
                 (acl2::nrev-finish acl2::nrev)))
             (mv x-res y-res memo acl2::nrev))
          (mv x-res y-res memo)))))
    (fast-alist-free memo)
    (mv x-res y-res)))))