Filtering...

macro-required-args-plus-tests

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

Included Books

macro-required-args-plus assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "macro-required-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-required-args+ 'tthm (w state)) '(fn))
other
(assert-equal (macro-required-args+ 'list (w state)) nil)
other
(assert-equal (macro-required-args+ 'defun (w state)) nil)
other
(assert-equal (macro-required-args+ 'defthm (w state))
  '(name term))
other
(assert-equal (macro-required-args+ 'defun-sk (w state))
  '(name args))
other
(must-succeed* (defmacro m (a) `(list ,A))
  (assert-equal (macro-required-args+ 'm (w state)) '(a)))
other
(must-succeed* (defmacro m (a &key b) `(list ,A ,(OR B :DEFAULT)))
  (assert-equal (macro-required-args+ 'm (w state)) '(a)))
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-required-args+ 'm (w state)) '(a)))