acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / make-event / test-case-check.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (TEST-CASE (+ 3 4)) (MAKE-EVENT (LET ((ASSERTION (+ 3 4))) (ER-PROGN (IF ASSERTION (VALUE NIL) (ER SOFT (QUOTE ASSERTION) "Assertion failed:~%~x0" (QUOTE (ASSERT!! (+ 3 4))))) (VALUE (QUOTE (VALUE-TRIPLE NIL))))) :CHECK-EXPANSION (VALUE-TRIPLE NIL) :ON-BEHALF-OF (ASSERT!! (+ 3 4)))) (4 RECORD-EXPANSION (TEST-CASE (+ 3 4) :EXPECTED 7) (MAKE-EVENT (LET ((ASSERTION (EQUAL (+ 3 4) 7))) (ER-PROGN (IF ASSERTION (VALUE NIL) (ER SOFT (QUOTE ASSERTION) "Assertion failed:~%~x0" (QUOTE (ASSERT!! (EQUAL (+ 3 4) 7))))) (VALUE (QUOTE (VALUE-TRIPLE NIL))))) :CHECK-EXPANSION (VALUE-TRIPLE NIL) :ON-BEHALF-OF (ASSERT!! (EQUAL (+ 3 4) 7)))) (5 RECORD-EXPANSION (MUST-FAIL (TEST-CASE (+ 3 4) :EXPECTED 8)) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (TEST-CASE (+ 3 4) :EXPECTED 8) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (TEST-CASE (+ 3 4) :EXPECTED 8) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (TEST-CASE (+ 3 4) :EXPECTED 8) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
                      expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (TEST-CASE (+ 3 4) :EXPECTED 8) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (TEST-CASE (+ 3 4) :EXPECTED 8)))) (6 RECORD-EXPANSION (TEST-CASE (EQUAL (+ 3 4) 7)) (MAKE-EVENT (LET ((ASSERTION (EQUAL (+ 3 4) 7))) (ER-PROGN (IF ASSERTION (VALUE NIL) (ER SOFT (QUOTE ASSERTION) "Assertion failed:~%~x0" (QUOTE (ASSERT!! (EQUAL (+ 3 4) 7))))) (VALUE (QUOTE (VALUE-TRIPLE NIL))))) :CHECK-EXPANSION (VALUE-TRIPLE NIL) :ON-BEHALF-OF (ASSERT!! (EQUAL (+ 3 4) 7)))) (7 RECORD-EXPANSION (MUST-FAIL (TEST-CASE (EQUAL (+ 3 4) 8))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (TEST-CASE (EQUAL (+ 3 4) 8)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (TEST-CASE (EQUAL (+ 3 4) 8)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (LET ((EXPR-VAL (CHECK-VARS-NOT-FREE (FORM-VAL-USE-NOWHERE-ELSE) T))) (COND ((EQ FORM-VAL-USE-NOWHERE-ELSE EXPR-VAL) (VALUE (LIST (QUOTE VALUE-TRIPLE) (LIST (QUOTE QUOTE) EXPR-VAL)))) (T (ER SOFT (MSG "( MUST-EVAL-TO ~@0 ~@1)" (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE (MV-LET (ERP VAL STATE) (TEST-CASE (EQUAL (+ 3 4) 8)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) (TILDE-@-ABBREVIATE-OBJECT-PHRASE (QUOTE T))) "Evaluation returned ~X01, not the value ~x2 of the ~
                      expression ~x3." FORM-VAL-USE-NOWHERE-ELSE (EVISC-TUPLE 4 3 NIL NIL) EXPR-VAL (QUOTE T)))))) :CHECK-EXPANSION (VALUE-TRIPLE (QUOTE T)) :ON-BEHALF-OF (MUST-EVAL-TO (MV-LET (ERP VAL STATE) (TEST-CASE (EQUAL (+ 3 4) 8)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (TEST-CASE (EQUAL (+ 3 4) 8))))))
NIL
(("/usr/share/acl2-6.3/books/make-event/test-case-check.lisp" "test-case-check" "test-case-check" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1097401012) ("/usr/share/acl2-6.3/books/make-event/assert-check.lisp" "assert-check" "assert-check" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 735978796) ("/usr/share/acl2-6.3/books/make-event/eval-check.lisp" "eval-check" "eval-check" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 309385933))
2098006203