		Search-engine friendly clone of the ACL2 documentation.

Parse-demo2-opts

Parse-demo2-opts-short->long

Signature
(parse-demo2-opts-short->long getopt::alias) → (mv getopt::errmsg? getopt::longname)
Arguments: getopt::alias — Guard (characterp getopt::alias).
Returns: getopt::longname — Type (stringp getopt::longname).

Definitions and Theorems

Function: parse-demo2-opts-short->long

(defun parse-demo2-opts-short->long (getopt::alias)
  (declare (xargs :guard (characterp getopt::alias)))
  (let ((acl2::__function__ 'parse-demo2-opts-short->long))
    (declare (ignorable acl2::__function__))
    (b* ((getopt::look (assoc getopt::alias
                              '((#\h . "help")
                                (#\v . "version")
                                (#\f . "fail"))))
         ((when getopt::look)
          (mv nil (cdr getopt::look))))
      (mv (msg "Unrecognized option -~s0."
               (acl2::implode (list getopt::alias)))
          ""))))

Theorem: stringp-of-parse-demo2-opts-short->long.longname

(defthm stringp-of-parse-demo2-opts-short->long.longname
  (b* (((mv getopt::?errmsg? getopt::?longname)
        (parse-demo2-opts-short->long getopt::alias)))
    (stringp getopt::longname))
  :rule-classes :type-prescription)