		Search-engine friendly clone of the ACL2 documentation.

Uninterpreted

Make-uninterpreted

Basic constructor macro for uninterpreted structures.

Syntax

(make-uninterpreted [:returns <returns>] 
                    [:more-returns <more-returns>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-uninterpreted

(defmacro make-uninterpreted (&rest args)
  (std::make-aggregate 'uninterpreted
                       args '((:returns) (:more-returns))
                       'make-uninterpreted
                       nil))

Function: uninterpreted

(defun uninterpreted (returns more-returns)
  (declare (xargs :guard (and (hint-pair-listp returns)
                              (hint-pair-listp more-returns))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'uninterpreted))
    (declare (ignorable acl2::__function__))
    (b* ((returns (mbe :logic (hint-pair-list-fix returns)
                       :exec returns))
         (more-returns (mbe :logic (hint-pair-list-fix more-returns)
                            :exec more-returns)))
      (list (cons 'returns returns)
            (cons 'more-returns more-returns)))))