(parse-vl-server-opts-short->long getopt::alias) → (mv getopt::errmsg? getopt::longname)
Function:
(defun parse-vl-server-opts-short->long (getopt::alias) (declare (xargs :guard (characterp getopt::alias))) (let ((__function__ 'parse-vl-server-opts-short->long)) (declare (ignorable __function__)) (b* ((getopt::look (assoc getopt::alias '((#\h . "help") (nil . "readme") (#\m . "mem") (#\p . "port") (#\r . "root") (nil . "public")))) ((when getopt::look) (mv nil (cdr getopt::look)))) (mv (msg "Unrecognized option -~s0." (implode (list getopt::alias))) ""))))
Theorem:
(defthm stringp-of-parse-vl-server-opts-short->long.longname (b* (((mv getopt::?errmsg? getopt::?longname) (parse-vl-server-opts-short->long getopt::alias))) (stringp getopt::longname)) :rule-classes :type-prescription)