• 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

Honsed-demo

Raw constructor for honsed demo-p structures.

Syntax:

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

This is identical to demo, except that we hons the structure we are creating.

Definition

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

Function: honsed-demo

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