		Search-engine friendly clone of the ACL2 documentation.

Get-option

Get-option-member

Process an option whose (optional) argument is a MEMBER of a set of choices.

This function checks for an option that may be specified as either :OPTION, (:OPTION), or (:OPTION choice), where in the latter form the choice must be a member of the set of choices. The choice is returned if the option is specified by the latter form, otherwise the default-if-missing is returned if the option is not present in the option-list, and default-if-unspecified is returned if the option if specified as :OPTION or (:OPTION).

Definitions and Theorems

Function: get-option-member

(defun get-option-member (ctx option
                              option-list choices default-if-missing
                              default-if-unspecified)
  (declare (xargs :guard (and (keywordp option)
                              (keyword-option-listp option-list)
                              (eqlable-listp choices))))
  (mv-let
        (msg value)
        (get-option-member-mv option
                              option-list choices default-if-missing
                              default-if-unspecified)
    (if msg (bomb ctx "~@0" msg) value)))