		Search-engine friendly clone of the ACL2 documentation.

Svex-override

Make-svex-override

Basic constructor macro for svex-override structures.

Syntax

(make-svex-override [:wire <wire>] 
                    [:test <test>] 
                    [:val <val>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svex-override

(defmacro make-svex-override (&rest args)
  (std::make-aggregate 'svex-override
                       args '((:wire) (:test) (:val))
                       'make-svex-override
                       nil))

Function: svex-override

(defun svex-override (wire test val)
  (declare (xargs :guard (and (svex-p wire)
                              (svex-p test)
                              (svex-p val))))
  (declare (xargs :guard t))
  (let ((__function__ 'svex-override))
    (declare (ignorable __function__))
    (b* ((wire (mbe :logic (svex-fix wire) :exec wire))
         (test (mbe :logic (svex-fix test) :exec test))
         (val (mbe :logic (svex-fix val) :exec val)))
      (list (cons 'wire wire)
            (cons 'test test)
            (cons 'val val)))))