		Search-engine friendly clone of the ACL2 documentation.

Svtv-composedata

Make-svtv-composedata

Basic constructor macro for svtv-composedata structures.

Syntax

(make-svtv-composedata [:simp <simp>] 
                       [:nextstates <nextstates>] 
                       [:input-substs <input-substs>])

This is the usual way to construct svtv-composedata structures. It simply conses together a structure with the specified fields.

This macro generates a new svtv-composedata structure from scratch. See also change-svtv-composedata, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-composedata

(defmacro make-svtv-composedata (&rest args)
  (std::make-aggregate 'svtv-composedata
                       args
                       '((:simp) (:nextstates) (:input-substs))
                       'make-svtv-composedata
                       nil))

Function: svtv-composedata

(defun svtv-composedata (simp nextstates input-substs)
  (declare (xargs :guard (and (svex-simpconfig-p simp)
                              (svex-alistlist-p nextstates)
                              (svex-alistlist-p input-substs))))
  (declare (xargs :guard t))
  (let ((__function__ 'svtv-composedata))
    (declare (ignorable __function__))
    (b* ((simp (mbe :logic (svex-simpconfig-fix simp)
                    :exec simp))
         (nextstates (mbe :logic (svex-alistlist-fix nextstates)
                          :exec nextstates))
         (input-substs (mbe :logic (svex-alistlist-fix input-substs)
                            :exec input-substs)))
      (std::prod-cons simp
                      (std::prod-cons nextstates input-substs)))))