• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
          • Defoptions
          • Demo2
            • Demo2-opts-p
              • Parse-demo2-opts
              • Demo2-opts
              • Make-demo2-opts
                • Change-demo2-opts
                • Make-honsed-demo2-opts
                • Honsed-demo2-opts
                • *demo2-opts-usage*
                • Demo2-opts->version
                • Demo2-opts->help
                • Demo2-opts->fail
              • Demo2-main
            • 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
    • Demo2-opts-p

    Make-demo2-opts

    Constructor macro for demo2-opts-p structures.

    Syntax:

    (make-demo2-opts [:help <help>] 
                     [:version <version>] 
                     [:fail <fail>]) 
    

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

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

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

    Definition

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

    Macro: make-demo2-opts

    (defmacro make-demo2-opts (&rest args)
      (std::make-aggregate 'demo2-opts
                           args '((:help) (:version) (:fail))
                           'make-demo2-opts
                           nil))