Basic constructor macro for bexp-not structures.
(make-bexp-not [:arg <arg>])
This is the usual way to construct bexp-not structures. It simply conses together a structure with the specified fields.
This macro generates a new bexp-not structure from scratch. See also change-bexp-not, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-bexp-not (&rest args) (std::make-aggregate 'bexp-not args '((:arg)) 'make-bexp-not nil))
Function:
(defun bexp-not (arg) (declare (xargs :guard (bexpp arg))) (declare (xargs :guard t)) (let ((__function__ 'bexp-not)) (declare (ignorable __function__)) (b* ((arg (mbe :logic (bexp-fix arg) :exec arg))) (cons :not (list arg)))))