		Search-engine friendly clone of the ACL2 documentation.

Std/testing

Must-not-be-table-key

A top-level assert$-like command to ensure that a table does not include a certain key.

Macro: must-not-be-table-key

(defmacro must-not-be-table-key (key table)
 (declare (xargs :guard (and (symbolp key) (symbolp table))))
 (cons
  'assert!
  (cons
   (cons
    'not
    (cons
       (cons 'assoc-eq
             (cons (cons 'quote (cons key 'nil))
                   (cons (cons 'table-alist
                               (cons (cons 'quote (cons table 'nil))
                                     '((w state))))
                         'nil)))
       'nil))
   'nil)))