Filtering...

macro-keyword-args-plus-tests

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

Included Books

macro-keyword-args-plus assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "macro-keyword-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-keyword-args+ 'tthm (w state)) nil)
other
(assert-equal (macro-keyword-args+ 'list (w state)) nil)
other
(assert-equal (macro-keyword-args+ 'defun (w state)) nil)
other
(assert-equal (macro-keyword-args+ 'defthm (w state))
  '((rule-classes :rewrite) (instructions) (hints) (otf-flg)))
other
(assert-equal (macro-keyword-args+ 'defun-sk (w state)) nil)
other
(must-succeed* (defmacro m (a) `(list ,A))
  (assert-equal (macro-keyword-args+ 'm (w state)) nil))
other
(must-succeed* (defmacro m (a &key b) `(list ,A ,(OR B :DEFAULT)))
  (assert-equal (macro-keyword-args+ 'm (w state)) '((b))))
other
(must-succeed* (defmacro m
    (&whole form a &optional b &key c (d '3) (e '#\e e-p))
    `(list ,A ,B ,C ,D ,E ,E-P ,FORM))
  (assert-equal (macro-keyword-args+ 'm (w state))
    '((c) (d . 3) (e . #\e))))