		Search-engine friendly clone of the ACL2 documentation.

Demo2-opts-p

Make-honsed-demo2-opts

Constructor macro for honsed demo2-opts-p structures.

Syntax:

(make-honsed-demo2-opts [:help <help>] 
                        [:version <version>] 
                        [:fail <fail>])

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

Definition

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

Macro: make-honsed-demo2-opts

(defmacro make-honsed-demo2-opts (&rest args)
  (std::make-aggregate 'demo2-opts
                       args '((:help) (:version) (:fail))
                       'make-honsed-demo2-opts
                       t))