Filtering...

ibody-tests

books/std/system/ibody-tests

Included Books

ibody assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "ibody")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (ibody 'not (w state))
  '(if p
    nil
    t))
other
(assert-equal (ibody 'len (w state))
  '(if (consp x)
    (+ 1 (len (cdr x)))
    0))
other
(must-succeed* (defun f (x) (+ x (list x x)))
  (assert-equal (ibody 'f (w state)) '(+ x (list x x))))