• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • 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
      • 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))