		Search-engine friendly clone of the ACL2 documentation.

Getopt

Formal->usage

Signature
(formal->usage x) → usage
Arguments: x — Guard (formal-p x).
Returns: usage — Type (stringp usage).

Definitions and Theorems

Function: formal->usage

(defun formal->usage (x)
  (declare (xargs :guard (formal-p x)))
  (let ((__function__ 'formal->usage))
    (declare (ignorable __function__))
    (b* (((formal x) x))
      (or (cdr (assoc :usage x.opts))
          x.doc))))