(parse-demo2-opts-short->long getopt::alias) → (mv getopt::errmsg? getopt::longname)
Function:
(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:
(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)