(parse-vl-lintconfig-short->long getopt::alias) → (mv getopt::errmsg? getopt::longname)
Function:
(defun parse-vl-lintconfig-short->long (getopt::alias) (declare (xargs :guard (characterp getopt::alias))) (let ((__function__ 'parse-vl-lintconfig-short->long)) (declare (ignorable __function__)) (b* ((getopt::look (assoc getopt::alias '((#\h . "help") (nil . "readme") (#\s . "search") (nil . "searchext") (#\I . "incdir") (nil . "topmod") (#\q . "quiet") (#\d . "drop") (#\i . "ignore") (nil . "ignore-file") (#\D . "define") (nil . "cclimit") (nil . "global-package") (nil . "elab-limit") (nil . "stmt-limit") (nil . "no-typo") (nil . "no-html") (nil . "no-sv-use-set") (nil . "edition") (nil . "strict") (#\m . "mem") (nil . "debug") (nil . "shell") (nil . "post-shell")))) ((when getopt::look) (mv nil (cdr getopt::look)))) (mv (msg "Unrecognized option -~s0." (implode (list getopt::alias))) ""))))
Theorem:
(defthm stringp-of-parse-vl-lintconfig-short->long.longname (b* (((mv getopt::?errmsg? getopt::?longname) (parse-vl-lintconfig-short->long getopt::alias))) (stringp getopt::longname)) :rule-classes :type-prescription)