		Search-engine friendly clone of the ACL2 documentation.

Demo2

Demo2-main

Run the demo2 program.

Definitions and Theorems

Function: demo2-main

(defun demo2-main (state)
 (b*
  (((mv argv state) (argv))
   ((mv errmsg opts ?extra-args)
    (parse-demo2-opts argv))
   ((when errmsg)
    (cw "~@0~%" errmsg)
    (exit 1)
    state)
   ((demo2-opts opts) opts)
   ((when opts.help)
    (b*
     ((-
        (cw "demo2: how to write a command line program in ACL2~%"))
      (state (princ$ *demo2-opts-usage* *standard-co* state))
      (- (cw "~%")))
     (exit 0)
     state))
   ((when opts.version)
    (cw "demo2: version 1.234~%")
    (exit 0)
    state)
   ((when opts.fail) (exit 1) state))
  (cw "colorless green ideas sleep furiously~%")
  (exit 0)
  state))