		Search-engine friendly clone of the ACL2 documentation.

Get-option

Get-option-check-syntax

Check the option list for gross syntax, returning NIL if it's OK, and crashing otherwise.

The argument option-list is the option list entered by the user. Valid-options is a list of keywords that specifies which options are valid. Duplicate-options is a list of keywords which specifies which options may be duplicated. Mutex-options is an alist of pairs (keyword1 . keyword2) which has the meaning `if keyword1 appears as an option then keyword2 may not appear as an option'.

Definitions and Theorems

Function: get-option-check-syntax

(defun get-option-check-syntax (ctx option-list valid-options
                                    duplicate-options mutex-options)
 (declare (xargs :guard (and (keyword-listp valid-options)
                             (keyword-listp duplicate-options)
                             (keyword-pair-alistp mutex-options))))
 (mv-let
       (msg flag)
       (get-option-check-syntax-mv option-list valid-options
                                   duplicate-options mutex-options)
  (declare (ignore flag))
  (if msg (bomb ctx
                "The keyword option list ~p0 is invalid because ~@1"
                option-list msg)
    nil)))