		Search-engine friendly clone of the ACL2 documentation.

Getopt

Sanity-check-formals

Make sure longnames and aliases are unique, every field has a parser, and so forth. This only applies to visible options.

Signature
(sanity-check-formals basename x world) → *
Arguments: basename — Guard (symbolp basename).; x — Guard (formallist-p x).; world — Guard (plist-worldp world).

Definitions and Theorems

Function: sanity-check-formals

(defun
     sanity-check-formals (basename x world)
     (declare (xargs :guard (and (symbolp basename)
                                 (formallist-p x)
                                 (plist-worldp world))))
     (let ((__function__ 'sanity-check-formals))
          (declare (ignorable __function__))
          (b* ((longnames (formallist->longnames x))
               ((unless (uniquep longnames))
                (raise "In ~x0, multiple fields have :longname ~&1."
                       basename
                       (duplicated-members longnames)))
               (aliases (remove nil (formallist->aliases x)))
               ((unless (uniquep aliases))
                (raise "In ~x0, multiple fields have :alias ~&1."
                       basename (duplicated-members aliases)))
               (?parsers (formallist->parsers x world))
               (?merges (formallist->merges x)))
              t)))