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

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (ASSERT!! (EQUAL 3 3) (DEFUN ASSERT-TEST1 (X) X)) (MAKE-EVENT (LET ((ASSERTION (EQUAL 3 3))) (ER-PROGN (IF ASSERTION (VALUE NIL) (ER SOFT (QUOTE ASSERTION) "Assertion failed:~%~x0" (QUOTE (ASSERT!! (EQUAL 3 3) (DEFUN ASSERT-TEST1 (X) X))))) (VALUE (QUOTE (DEFUN ASSERT-TEST1 (X) X))))) :CHECK-EXPANSION (DEFUN ASSERT-TEST1 (X) X) :ON-BEHALF-OF (ASSERT!! (EQUAL 3 3) (DEFUN ASSERT-TEST1 (X) X)))) (6 RECORD-EXPANSION (MUST-FAIL (ASSERT!! (EQUAL 3 4) (DEFUN ASSERT-TEST2 (X) X))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (ASSERT!! (EQUAL 3 4) (DEFUN ASSERT-TEST2 (X) X)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (ASSERT!! (EQUAL 3 4) (DEFUN ASSERT-TEST2 (X) X)) (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) (ASSERT!! (EQUAL 3 4) (DEFUN ASSERT-TEST2 (X) X)) (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) (ASSERT!! (EQUAL 3 4) (DEFUN ASSERT-TEST2 (X) X)) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (ASSERT!! (EQUAL 3 4) (DEFUN ASSERT-TEST2 (X) X))))) (8 RECORD-EXPANSION (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B C D E F)))) (MAKE-EVENT (LET ((ASSERTION (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B C D E F))))) (ER-PROGN (IF ASSERTION (VALUE NIL) (ER SOFT (QUOTE ASSERTION) "Assertion failed:~%~x0" (QUOTE (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B C D E F))))))) (VALUE (QUOTE (VALUE-TRIPLE NIL))))) :CHECK-EXPANSION (VALUE-TRIPLE NIL) :ON-BEHALF-OF (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B C D E F)))))) (9 RECORD-EXPANSION (MUST-FAIL (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B))))) (MAKE-EVENT (QUOTE (MUST-EVAL-TO-T (MV-LET (ERP VAL STATE) (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))))) :CHECK-EXPANSION (MAKE-EVENT (ER-LET* ((FORM-VAL-USE-NOWHERE-ELSE (MV-LET (ERP VAL STATE) (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B)))) (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) (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B)))) (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) (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B)))) (DECLARE (IGNORE VAL)) (VALUE (NOT (EQ ERP NIL)))) T)) :ON-BEHALF-OF (MUST-FAIL (ASSERT!! (EQUAL (APPEND (QUOTE (A B C)) (QUOTE (D E F))) (QUOTE (A B))))))) (11 RECORD-EXPANSION (ASSERT!! (EQUAL (ACCESS-COMMAND-TUPLE-FORM (CDDR (CAR (SCAN-TO-COMMAND (W STATE))))) (QUOTE (EXIT-BOOT-STRAP-MODE)))) (MAKE-EVENT (LET ((ASSERTION (EQUAL (ACCESS-COMMAND-TUPLE-FORM (CDDR (CAR (SCAN-TO-COMMAND (W STATE))))) (QUOTE (EXIT-BOOT-STRAP-MODE))))) (ER-PROGN (IF ASSERTION (VALUE NIL) (ER SOFT (QUOTE ASSERTION) "Assertion failed:~%~x0" (QUOTE (ASSERT!! (EQUAL (ACCESS-COMMAND-TUPLE-FORM (CDDR (CAR (SCAN-TO-COMMAND (W STATE))))) (QUOTE (EXIT-BOOT-STRAP-MODE))))))) (VALUE (QUOTE (VALUE-TRIPLE NIL))))) :CHECK-EXPANSION (VALUE-TRIPLE NIL) :ON-BEHALF-OF (ASSERT!! (EQUAL (ACCESS-COMMAND-TUPLE-FORM (CDDR (CAR (SCAN-TO-COMMAND (W STATE))))) (QUOTE (EXIT-BOOT-STRAP-MODE)))))))
NIL
(("/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))
1908209009