		Search-engine friendly clone of the ACL2 documentation.

Support

Getarg+

Get a value from the keyword-value alist produced by extract-keywords, with default-value support, and additionally return a flag saying whether the key was bound. Returns (mv value boundp).

Definitions and Theorems

Function: getarg+

(defun getarg+ (arg default alist)
  (declare (xargs :guard (and (eqlablep arg) (alistp alist))))
  (b* ((look (assoc arg alist)))
    (if look (mv (cdr look) t)
      (mv default nil))))