Filtering...

install-not-normalized-event-tests

books/std/system/install-not-normalized-event-tests

Included Books

install-not-normalized-event theorem-namep assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "install-not-normalized-event")
include-book
(include-book "theorem-namep")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (mv-list 3
    (install-not-normalized-event 'f nil nil (w state)))
  '((install-not-normalized f
     :defthm-name 'f$not-normalized
     :allp nil) f$not-normalized
    (f$not-normalized)))
other
(assert-equal (mv-list 3
    (install-not-normalized-event 'g t nil (w state)))
  '((local (install-not-normalized g
       :defthm-name 'g$not-normalized
       :allp nil)) g$not-normalized
    (g$not-normalized)))
other
(assert-equal (mv-list 3
    (install-not-normalized-event 'f nil '(a b) (w state)))
  '((install-not-normalized f
     :defthm-name 'f$not-normalized
     :allp nil) f$not-normalized
    (f$not-normalized a b)))
other
(assert-equal (mv-list 3
    (install-not-normalized-event 'f
      nil
      '(a f$not-normalized)
      (w state)))
  '((install-not-normalized f
     :defthm-name 'f$not-normalized$
     :allp nil) f$not-normalized$
    (f$not-normalized$ a f$not-normalized)))
other
(must-succeed* (defun f$not-normalized (x) x)
  (assert-equal (mv-list 3
      (install-not-normalized-event 'f nil nil (w state)))
    '((install-not-normalized f
       :defthm-name 'f$not-normalized$
       :allp nil) f$not-normalized$
      (f$not-normalized$))))
other
(must-succeed* (defun f$not-normalized (x) x)
  (defun f$not-normalized$ (x) x)
  (assert-equal (mv-list 3
      (install-not-normalized-event 'f nil nil (w state)))
    '((install-not-normalized f
       :defthm-name 'f$not-normalized$$
       :allp nil) f$not-normalized$$
      (f$not-normalized$$))))
other
(must-succeed* (defun f (x) x)
  (make-event (b* (((mv event & &) (install-not-normalized-event 'f nil nil (w state))))
      event))
  (assert! (theorem-namep 'f$not-normalized (w state))))
other
(must-succeed* (defun g (x) x)
  (encapsulate nil
    (make-event (b* (((mv event & &) (install-not-normalized-event 'g t nil (w state))))
        event))
    (assert! (theorem-namep 'g$not-normalized (w state))))
  (assert! (not (theorem-namep 'g$not-normalized (w state)))))
other
(must-succeed* (defun f (x) x)
  (make-event (b* (((mv event & &) (install-not-normalized-event 'f nil '(a b) (w state))))
      event))
  (assert! (theorem-namep 'f$not-normalized (w state))))
other
(must-succeed* (defun f (x) x)
  (make-event (b* (((mv event & &) (install-not-normalized-event 'f
           nil
           '(a f$not-normalized)
           (w state))))
      event))
  (assert! (theorem-namep 'f$not-normalized$ (w state))))
other
(must-succeed* (defun f (x) x)
  (defun f$not-normalized (x) x)
  (make-event (b* (((mv event & &) (install-not-normalized-event 'f nil nil (w state))))
      event))
  (assert! (theorem-namep 'f$not-normalized$ (w state))))
other
(must-succeed* (defun f (x) x)
  (defun f$not-normalized (x) x)
  (defun f$not-normalized$ (x) x)
  (make-event (b* (((mv event & &) (install-not-normalized-event 'f nil nil (w state))))
      event))
  (assert! (theorem-namep 'f$not-normalized$$ (w state))))