• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Std/io
      • Oslib
      • Bridge
      • Clex
      • Tshell
      • Unsound-eval
      • Hacker
      • ACL2s-interface
      • Startup-banner
      • Command-line
        • Save-exec
        • Argv
        • Getopt
          • Demo-p
            • Parse-demo
            • Demo
            • Make-demo
              • Change-demo
              • Honsed-demo
              • Make-honsed-demo
              • *demo-usage*
              • Demo->version
              • Demo->verbose
              • Demo->username
              • Demo->port
              • Demo->help
              • Demo->extra-stuff2
              • Demo->extra-stuff
              • Demo->dirs
            • Defoptions
            • Demo2
            • Parsers
            • Sanity-check-formals
            • Formal->parser
            • Formal->argname
            • Formal->longname
            • Formal->alias
            • Formal->usage
            • Formal->merge
            • Formal->hiddenp
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Demo-p

    Make-demo

    Constructor macro for demo-p structures.

    Syntax:

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

    This is our preferred way to construct demo-p structures. It simply conses together a structure with the specified fields.

    This macro generates a new demo-p structure from scratch. See also change-demo, which can "change" an existing structure, instead.

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

    Definition

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

    Macro: make-demo

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