• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Oslib
      • Std/io
      • Bridge
      • Clex
      • Tshell
      • Unsound-eval
      • Hacker
      • 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->merge
            • Formal->alias
            • Formal->usage
            • Formal->hiddenp
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Demo2-opts-p

    Demo2-opts

    Raw constructor for demo2-opts-p structures.

    Syntax:

    (demo2-opts help version fail)

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

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

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

    Definition

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

    Function: demo2-opts

    (defun demo2-opts (help version fail)
           (declare (xargs :guard (and (booleanp help)
                                       (booleanp version)
                                       (booleanp fail))))
           (cons :demo2 (cons (cons 'help help)
                              (cons (cons 'version version)
                                    (cons (cons 'fail fail) nil)))))