unwrapped-nonexec-body-tests

Included Books

unwrapped-nonexec-body assert-equal must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "unwrapped-nonexec-body")

include-book

(include-book "std/testing/assert-equal" :dir :system)

include-book

(include-book "std/testing/must-succeed-star" :dir :system)

other

(must-succeed* (defun-nx f (x) (cons (list x) (list x)))
  (assert-equal (ubody 'f (w state))
    '(return-last 'progn
      (throw-nonexec-error 'f (cons x 'nil))
      (cons (cons x 'nil) (cons x 'nil))))
  (assert-equal (unwrapped-nonexec-body 'f (w state))
    '(cons (cons x 'nil) (cons x 'nil))))