Function:
(defun vl-toolkit-help-message-default (command) (declare (xargs :guard (stringp command))) (let ((__function__ 'vl-toolkit-help-message-default)) (declare (ignorable __function__)) (cdr (assoc-equal command *vl-help-messages*))))
Theorem:
(defthm return-type-of-vl-toolkit-help-message-default (b* ((help (vl-toolkit-help-message-default command))) (or (not help) (stringp help))) :rule-classes :type-prescription)