Filtering...

must-be-table-key

books/std/testing/must-be-table-key

Included Books

assert-bang
other
(in-package "ACL2")
include-book
(include-book "assert-bang")
other
(defsection must-be-table-key
  :parents (std/testing)
  :short "A top-level @(tsee assert$)-like command to ensure that
          a @(see table) includes a certain key."
  :long "@(def must-be-table-key)"
  (defmacro must-be-table-key
    (key table)
    (declare (xargs :guard (and (symbolp key) (symbolp table))))
    `(assert! (assoc-eq ',KEY (table-alist ',TABLE (w state))))))