Filtering...

with-supporters-test-top

books/tools/with-supporters-test-top

Included Books

with-supporters
other
(in-package "ACL2")
include-book
(include-book "with-supporters")
other
(deflabel my-start)
local
(local (progn (defun f1 (x) (declare (xargs :guard t)) x)
    (defund f2
      (x)
      (declare (xargs :guard (f1 x)))
      (if (and (consp x) (consp (cdr x)))
        (f2 (cdr x))
        x))
    (defun f3 (x) (f2 x))))
other
(with-supporters-after my-start
  (in-theory (enable (:d f2)))
  (defun h1 (x) (f3 x)))
other
(assert-event (equal (disabledp 'f2) '((:induction f2)))
  :on-skip-proofs t)
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  (defun h2 (x) (g3 x)))
other
(assert-event (equal (get-event 'g2 (w state))
    '(defun g2 (x) (declare (xargs :guard (g1 x))) (mac2 x))))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (g5))
other
(assert-event (equal (disabledp 'g4) '((:definition g4)))
  :on-skip-proofs t)
other
(assert-event (equal (g5 '(4 5 6)) 4) :on-skip-proofs t)
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  (defun h3 (st) (declare (xargs :stobjs st)) (fld st)))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (stub2))
other
(assert-event (and (equal (stub1 3) '(3 . 3)) (equal (stub2 3) '(3 3)))
  :on-skip-proofs t)
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  (defun h4
    (st)
    (declare (xargs :stobjs st))
    (update-fld 3 st)))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (stub1 stub3))
other
(assert-event (and (equal (stub1 3) '(3 . 3))
    (equal (stub2 3) '(3 3))
    (equal (stub3 '(a b c d)) 4))
  :on-skip-proofs t)
other
(assert-event (equal (disabledp 'g8) nil) :on-skip-proofs t)
other
(assert-event (equal (disabledp 'g9) '((:definition g9)))
  :on-skip-proofs t)
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (g11 g13)
  :show :only)
other
(assert-event (not (function-symbolp 'g10 (w state))))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (g11 g13)
  :show t)
other
(assert-event (function-symbolp 'g10 (w state)))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (mac))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :tables (my-tbl))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :with-output (:on :all)
  :tables :all)
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (e1))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (g16))
other
(with-supporters (local (include-book "with-supporters-test-sub"))
  :names (g18))