		Search-engine friendly clone of the ACL2 documentation.

Indname-result

Make-indname-result

Basic constructor macro for indname-result structures.

Syntax

(make-indname-result [:varname <varname>] 
                     [:decl <decl>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-indname-result

(defmacro make-indname-result (&rest args)
  (std::make-aggregate 'indname-result
                       args '((:varname) (:decl))
                       'make-indname-result
                       nil))

Function: indname-result

(defun indname-result (varname decl)
  (declare (xargs :guard (and (svar-p varname) (wire-p decl))))
  (declare (xargs :guard t))
  (let ((__function__ 'indname-result))
    (declare (ignorable __function__))
    (b* ((varname (mbe :logic (svar-fix varname)
                       :exec varname))
         (decl (mbe :logic (wire-fix decl)
                    :exec decl)))
      (cons varname decl))))