Filtering...

macro-args-plus-tests

books/std/system/macro-args-plus-tests

Included Books

macro-args-plus assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "macro-args-plus")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (macro-args+ 'list (w state)) '(&rest args))
other
(must-succeed* (defmacro mac
    (x y z &key a (b '3) (c '(#\a 1/3) cp))
    (list x y z a b c cp))
  (assert-equal (macro-args+ 'mac (w state))
    '(x y z &key a (b '3) (c '(#\a 1/3) cp))))