		Search-engine friendly clone of the ACL2 documentation.

Demo-p

Make-honsed-demo

Constructor macro for honsed demo-p structures.

Syntax:

(make-honsed-demo [:help <help>] 
                  [:verbose <verbose>] 
                  [:version <version>] 
                  [:username <username>] 
                  [:port <port>] 
                  [:dirs <dirs>] 
                  [:extra-stuff <extra-stuff>] 
                  [:extra-stuff2 <extra-stuff2>])

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

Definition

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

Macro: make-honsed-demo

(defmacro make-honsed-demo (&rest args)
  (std::make-aggregate 'demo
                       args
                       '((:help)
                         (:verbose)
                         (:version)
                         (:username . "")
                         (:port . 55432)
                         (:dirs)
                         (:extra-stuff)
                         (:extra-stuff2 . ""))
                       'make-honsed-demo
                       t))