Filtering...

defund-sk-tests

books/std/util/defund-sk-tests

Included Books

defund-sk assert-bang must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "defund-sk")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(must-succeed* (defund-sk f (x) (forall y (equal x y)))
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f (x) (forall y (equal x y)) :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f (x) (forall y (equal x y)) :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-necc))))
other
(must-succeed* (defund-sk f (x) (forall y (equal x y)) :constrain nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain nil
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain nil
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-necc))))
other
(must-succeed* (defund-sk f (x) (forall y (equal x y)) :constrain t)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain t
    :thm-enable nil)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain t
    :thm-enable t)
  (assert! (disabledp 'f-definition))
  (assert! (not (disabledp 'f-necc))))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule
    :thm-enable nil)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule
    :thm-enable t)
  (assert! (disabledp 'f-def-rule))
  (assert! (not (disabledp 'f-necc))))
other
(must-succeed* (defund-sk f (x) (forall y (equal x y)) :thm-name nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :thm-name nil
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-necc))))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain nil
    :thm-name nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain nil
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain nil
    :thm-name nil
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-necc))))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain t
    :thm-name nil)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain t
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain t
    :thm-name nil
    :thm-enable t)
  (assert! (disabledp 'f-definition))
  (assert! (not (disabledp 'f-necc))))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-necc)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule
    :thm-name nil
    :thm-enable t)
  (assert! (disabledp 'f-def-rule))
  (assert! (not (disabledp 'f-necc))))
other
(must-succeed* (defund-sk f (x) (forall y (equal x y)) :thm-name f-rw-rule)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :thm-name f-rw-rule
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :thm-name f-rw-rule
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-rw-rule))))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain nil
    :thm-name f-rw-rule)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain nil
    :thm-name f-rw-rule
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain nil
    :thm-name f-rw-rule
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-rw-rule))))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain t
    :thm-name f-rw-rule)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain t
    :thm-name f-rw-rule
    :thm-enable nil)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain t
    :thm-name f-rw-rule
    :thm-enable t)
  (assert! (disabledp 'f-definition))
  (assert! (not (disabledp 'f-rw-rule))))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule
    :thm-name f-rw-rule)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule
    :thm-name f-rw-rule
    :thm-enable nil)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (forall y (equal x y))
    :constrain f-def-rule
    :thm-name f-rw-rule
    :thm-enable t)
  (assert! (disabledp 'f-def-rule))
  (assert! (not (disabledp 'f-rw-rule))))
other
(must-succeed* (defund-sk f (x) (exists y (equal x y)))
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f (x) (exists y (equal x y)) :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f (x) (exists y (equal x y)) :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-suff))))
other
(must-succeed* (defund-sk f (x) (exists y (equal x y)) :constrain nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain nil
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain nil
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-suff))))
other
(must-succeed* (defund-sk f (x) (exists y (equal x y)) :constrain t)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain t
    :thm-enable nil)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain t
    :thm-enable t)
  (assert! (disabledp 'f-definition))
  (assert! (not (disabledp 'f-suff))))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule
    :thm-enable nil)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule
    :thm-enable t)
  (assert! (disabledp 'f-def-rule))
  (assert! (not (disabledp 'f-suff))))
other
(must-succeed* (defund-sk f (x) (exists y (equal x y)) :thm-name nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :thm-name nil
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-suff))))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain nil
    :thm-name nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain nil
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain nil
    :thm-name nil
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-suff))))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain t
    :thm-name nil)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain t
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain t
    :thm-name nil
    :thm-enable t)
  (assert! (disabledp 'f-definition))
  (assert! (not (disabledp 'f-suff))))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule
    :thm-name nil)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule
    :thm-name nil
    :thm-enable nil)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-suff)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule
    :thm-name nil
    :thm-enable t)
  (assert! (disabledp 'f-def-rule))
  (assert! (not (disabledp 'f-suff))))
other
(must-succeed* (defund-sk f (x) (exists y (equal x y)) :thm-name f-rw-rule)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :thm-name f-rw-rule
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :thm-name f-rw-rule
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-rw-rule))))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain nil
    :thm-name f-rw-rule)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain nil
    :thm-name f-rw-rule
    :thm-enable nil)
  (assert! (disabledp 'f))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain nil
    :thm-name f-rw-rule
    :thm-enable t)
  (assert! (disabledp 'f))
  (assert! (not (disabledp 'f-rw-rule))))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain t
    :thm-name f-rw-rule)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain t
    :thm-name f-rw-rule
    :thm-enable nil)
  (assert! (disabledp 'f-definition))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain t
    :thm-name f-rw-rule
    :thm-enable t)
  (assert! (disabledp 'f-definition))
  (assert! (not (disabledp 'f-rw-rule))))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule
    :thm-name f-rw-rule)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule
    :thm-name f-rw-rule
    :thm-enable nil)
  (assert! (disabledp 'f-def-rule))
  (assert! (disabledp 'f-rw-rule)))
other
(must-succeed* (defund-sk f
    (x)
    (exists y (equal x y))
    :constrain f-def-rule
    :thm-name f-rw-rule
    :thm-enable t)
  (assert! (disabledp 'f-def-rule))
  (assert! (not (disabledp 'f-rw-rule))))