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