		Search-engine friendly clone of the ACL2 documentation.

Wcp-template-p

Make-honsed-wcp-template

Constructor macro for honsed wcp-template-p structures.

Syntax:

(make-honsed-wcp-template [:name <name>] 
                          [:enabledp <enabledp>] 
                          [:pat <pat>] 
                          [:templ <templ>] 
                          [:rulenames <rulenames>] 
                          [:restriction <restriction>])

This is identical to make-wcp-template, except that we hons the structure we are creating.

Definition

This is an ordinary honsing make- macro introduced by std::defaggregate.

Macro: make-honsed-wcp-template

(defmacro make-honsed-wcp-template (&rest args)
  (std::make-aggregate 'wcp-template
                       args
                       '((:name)
                         (:enabledp)
                         (:pat)
                         (:templ)
                         (:rulenames)
                         (:restriction))
                       'make-honsed-wcp-template
                       t))