		Search-engine friendly clone of the ACL2 documentation.

Vl-lexscope-entry

Change-vl-lexscope-entry

Modifying constructor for vl-lexscope-entry structures.

Syntax

(change-vl-lexscope-entry x 
                          [:decl <decl>] 
                          [:direct-pkg <direct-pkg>] 
                          [:wildpkgs <wildpkgs>] 
                          [:genblockp <genblockp>])

This is an often useful alternative to make-vl-lexscope-entry.

We construct a new vl-lexscope-entry structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

This is an ordinary change- macro introduced by defprod.

Macro: change-vl-lexscope-entry

(defmacro change-vl-lexscope-entry (x &rest args)
  (std::change-aggregate
       'vl-lexscope-entry
       x args
       '((:decl . vl-lexscope-entry->decl)
         (:direct-pkg . vl-lexscope-entry->direct-pkg)
         (:wildpkgs . vl-lexscope-entry->wildpkgs)
         (:genblockp . vl-lexscope-entry->genblockp))
       'change-vl-lexscope-entry
       'remake-vl-lexscope-entry))