Filtering...

defmacro-plus-tests

books/std/util/defmacro-plus-tests

Included Books

defmacro-plus must-succeed
other
(in-package "ACL2")
include-book
(include-book "defmacro-plus")
include-book
(include-book "std/testing/must-succeed" :dir :system)
other
(must-succeed (defmacro+ mac (x y) `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac (x y) :parents nil `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac (x y) `(list ,X ,Y) :parents nil))
other
(must-succeed (defmacro+ mac (x y) :parents (some-parent) `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac (x y) `(list ,X ,Y) :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent another-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    `(list ,X ,Y)
    :parents (some-parent another-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents nil
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents nil
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :parents nil))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent another-parent)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent another-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :parents (some-parent another-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents nil
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents nil
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    :parents nil
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)
    :parents nil))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    :parents (some-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent another-parent)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent another-parent)
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    :parents (some-parent another-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)
    :parents (some-parent another-parent)))
other
(must-succeed (defmacro+ mac (x y) :short "a short string" `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac (x y) `(list ,X ,Y) :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    :short "a short string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)
    :short "a short string"))
other
(must-succeed (defmacro+ mac (x y) :long "a long string" `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac (x y) `(list ,X ,Y) :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    (declare (xargs :guard (stringp y)))
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :short "a short string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    `(list ,X ,Y)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    `(list ,X ,Y)
    :parents (some-parent)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    :parents (some-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    `(list ,X ,Y)
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    `(list ,X ,Y)
    :short "a short string"
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    :short "a short string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    `(list ,X ,Y)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :parents (some-parent)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    :parents (some-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    `(list ,X ,Y)
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :short "a short string"
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    `(list ,X ,Y)
    :parents (some-parent)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    :parents (some-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    `(list ,X ,Y)
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    `(list ,X ,Y)
    :long "a long string"
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :parents (some-parent)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    :parents (some-parent)
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    `(list ,X ,Y)
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :long "a long string"
    :parents (some-parent)))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    `(list ,X ,Y)
    :short "a short string"
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    :short "a short string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    `(list ,X ,Y)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    `(list ,X ,Y)
    :long "a long string"
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :short "a short string"
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    :short "a short string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    `(list ,X ,Y)
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :long "a long string"
    :short "a short string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :short "a short string"
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :short "a short string"
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    `(list ,X ,Y)
    :short "a short string"
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    `(list ,X ,Y)
    :parents (some-parent)
    :short "a short string"
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :short "a short string"
    :long "a long string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    :short "a short string"
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    :parents (some-parent)
    (declare (xargs :guard (symbolp x)))
    :short "a short string"
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    :short "a short string"
    :long "a long string"
    `(list ,X ,Y)))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    :short "a short string"
    `(list ,X ,Y)
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    :parents (some-parent)
    `(list ,X ,Y)
    :short "a short string"
    :long "a long string"))
other
(must-succeed (defmacro+ mac
    (x y)
    (declare (xargs :guard (symbolp x)))
    `(list ,X ,Y)
    :parents (some-parent)
    :short "a short string"
    :long "a long string"))