		Search-engine friendly clone of the ACL2 documentation.

Atc-premise-cvalues

Make-atc-premise-cvalues

Basic constructor macro for atc-premise-cvalues structures.

Syntax

(make-atc-premise-cvalues [:vars <vars>] 
                          [:term <term>])

This is the usual way to construct atc-premise-cvalues structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-atc-premise-cvalues

(defmacro make-atc-premise-cvalues (&rest args)
  (std::make-aggregate 'atc-premise-cvalues
                       args '((:vars) (:term))
                       'make-atc-premise-cvalues
                       nil))

Function: atc-premise-cvalues

(defun atc-premise-cvalues (vars term)
  (declare (xargs :guard (and (symbol-listp vars)
                              (acl2::any-p term))))
  (declare (xargs :guard t))
  (let ((__function__ 'atc-premise-cvalues))
    (declare (ignorable __function__))
    (b* ((vars (mbe :logic (symbol-list-fix vars)
                    :exec vars))
         (term (mbe :logic (identity term)
                    :exec term)))
      (cons :cvalues (list vars term)))))