		Search-engine friendly clone of the ACL2 documentation.

Demo-p

Honsed-demo

Raw constructor for honsed demo-p structures.

Syntax:

(honsed-demo help verbose version username
             port dirs extra-stuff extra-stuff2)

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

Definition

This is an ordinary honsing constructor introduced by std::defaggregate.

Function: honsed-demo

(defun honsed-demo (help verbose version username
                         port dirs extra-stuff extra-stuff2)
 (declare (xargs :guard (and (booleanp help)
                             (booleanp verbose)
                             (booleanp version)
                             (stringp username)
                             (natp port)
                             (string-listp dirs)
                             (stringp extra-stuff2))))
 (mbe
  :logic (demo help verbose version username
               port dirs extra-stuff extra-stuff2)
  :exec
  (hons
   :demo
   (hons
    (hons 'help help)
    (hons
     (hons 'verbose verbose)
     (hons
      (hons 'version version)
      (hons
           (hons 'username username)
           (hons (hons 'port port)
                 (hons (hons 'dirs dirs)
                       (hons (hons 'extra-stuff extra-stuff)
                             (hons (hons 'extra-stuff2 extra-stuff2)
                                   nil)))))))))))