		Search-engine friendly clone of the ACL2 documentation.

Demo-p

Demo

Raw constructor for demo-p structures.

Syntax:

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

This is the lowest-level constructor for demo-p structures. It simply conses together a structure with the specified fields.

Note: It's generally better to use macros like make-demo or change-demo instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

The demo-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-demo instead.

Definition

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

Function: demo

(defun 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))))
 (cons
  :demo
  (cons
   (cons 'help help)
   (cons
    (cons 'verbose verbose)
    (cons
     (cons 'version version)
     (cons (cons 'username username)
           (cons (cons 'port port)
                 (cons (cons 'dirs dirs)
                       (cons (cons 'extra-stuff extra-stuff)
                             (cons (cons 'extra-stuff2 extra-stuff2)
                                   nil))))))))))