		Search-engine friendly clone of the ACL2 documentation.

Vl-unparam-ledger

Make-vl-unparam-ledger

Basic constructor macro for vl-unparam-ledger structures.

Syntax

(make-vl-unparam-ledger [:ndb <ndb>] 
                        [:instkeymap <instkeymap>] 
                        [:omit-default-params <omit-default-params>])

This is the usual way to construct vl-unparam-ledger structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-unparam-ledger

(defmacro make-vl-unparam-ledger (&rest args)
  (std::make-aggregate 'vl-unparam-ledger
                       args
                       '((:ndb)
                         (:instkeymap)
                         (:omit-default-params))
                       'make-vl-unparam-ledger
                       nil))

Function: vl-unparam-ledger

(defun vl-unparam-ledger (ndb instkeymap omit-default-params)
 (declare (xargs :guard (and (vl-namedb-p ndb)
                             (vl-unparam-instkeymap-p instkeymap)
                             (booleanp omit-default-params))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-unparam-ledger))
   (declare (ignorable __function__))
   (b*
     ((ndb (mbe :logic (vl-namedb-fix ndb)
                :exec ndb))
      (instkeymap (mbe :logic (vl-unparam-instkeymap-fix instkeymap)
                       :exec instkeymap))
      (omit-default-params
           (mbe :logic (acl2::bool-fix omit-default-params)
                :exec omit-default-params)))
     (list (cons 'ndb ndb)
           (cons 'instkeymap instkeymap)
           (cons 'omit-default-params
                 omit-default-params)))))