		Search-engine friendly clone of the ACL2 documentation.

Modinst

Make-modinst

Basic constructor macro for modinst structures.

Syntax

(make-modinst [:instname <instname>] 
              [:modname <modname>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-modinst

(defmacro make-modinst (&rest args)
  (std::make-aggregate 'modinst
                       args '((:instname) (:modname))
                       'make-modinst
                       nil))

Function: modinst

(defun modinst (instname modname)
  (declare (xargs :guard (and (name-p instname)
                              (modname-p modname))))
  (declare (xargs :guard t))
  (let ((__function__ 'modinst))
    (declare (ignorable __function__))
    (b* ((instname (mbe :logic (name-fix instname)
                        :exec instname))
         (modname (mbe :logic (modname-fix modname)
                       :exec modname)))
      (std::prod-cons instname modname))))