acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / tools / defconsts.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((33 RECORD-EXPANSION (LOCAL (ENCAPSULATE NIL (DEFCONSTS *FOO* 1) (DEFCONSTS (*FOO*) 1) (DEFCONSTS (*FOO* *BAR*) (MV 1 2)) (DEFCONSTS (*FOO* *BAR* &) (MV 1 2 3)) (DEFCONSTS (*FOO* *BAR* & *BAZ*) (MV 1 2 3 4)) (DEFTHM FOO (EQUAL *FOO* 1) :RULE-CLASSES NIL) (DEFTHM BAR (EQUAL *BAR* 2) :RULE-CLASSES NIL) (DEFTHM BAZ (EQUAL *BAZ* 4) :RULE-CLASSES NIL))) (LOCAL (VALUE-TRIPLE :ELIDED))) (34 RECORD-EXPANSION (LOCAL (ENCAPSULATE NIL (DEFCONSTS STATE (MV-LET (COL STATE) (FMT "Hello, world!~%" NIL *STANDARD-CO* STATE NIL) (DECLARE (IGNORE COL)) STATE)) (DEFCONSTS (STATE) (MV-LET (COL STATE) (FMT "Hello, world!~%" NIL *STANDARD-CO* STATE NIL) (DECLARE (IGNORE COL)) STATE)) (DEFCONSTS (*HUNDRED* STATE) (MV-LET (COL STATE) (FMT "Hello, world!~%" NIL *STANDARD-CO* STATE NIL) (DECLARE (IGNORE COL)) (MV 100 STATE))) (DEFCONSTS (STATE *HUNDRED*) (MV-LET (COL STATE) (FMT "Hello, world!~%" NIL *STANDARD-CO* STATE NIL) (DECLARE (IGNORE COL)) (MV STATE 100))) (DEFTHM HUNDRED (EQUAL *HUNDRED* 100) :RULE-CLASSES NIL))) (LOCAL (VALUE-TRIPLE :ELIDED))) (35 RECORD-EXPANSION (LOCAL (ENCAPSULATE NIL (DEFSTOBJ MYSTOBJ (FIELD :INITIALLY 0)) (DEFCONSTS *ZERO* (FIELD MYSTOBJ)) (DEFCONSTS MYSTOBJ (UPDATE-FIELD 3 MYSTOBJ)) (DEFCONSTS *THREE* (FIELD MYSTOBJ)) (DEFCONSTS (*FIVE* MYSTOBJ STATE) (MV-LET (COL STATE) (FMT "Hello, world!~%" NIL *STANDARD-CO* STATE NIL) (DECLARE (IGNORE COL)) (LET ((MYSTOBJ (UPDATE-FIELD 5 MYSTOBJ))) (MV (FIELD MYSTOBJ) MYSTOBJ STATE)))) (DEFTHM T1 (EQUAL *ZERO* 0) :RULE-CLASSES NIL) (DEFTHM T2 (EQUAL *THREE* 3) :RULE-CLASSES NIL) (DEFTHM T3 (EQUAL *FIVE* 5) :RULE-CLASSES NIL))) (LOCAL (VALUE-TRIPLE :ELIDED))) (36 RECORD-EXPANSION (LOCAL (ENCAPSULATE NIL (DEFCONSTS *OOPS* __FUNCTION__) (DEFCONSTS (*OOPS2* STATE) (MV __FUNCTION__ STATE)) (DEFTHM F1 (EQUAL *OOPS* (QUOTE |(DEFCONSTS *OOPS* ...)|)) :RULE-CLASSES NIL) (DEFTHM F2 (EQUAL *OOPS2* (QUOTE |(DEFCONSTS (*OOPS2* ...) ...)|)) :RULE-CLASSES NIL))) (LOCAL (VALUE-TRIPLE :ELIDED))))
NIL
(("/usr/share/acl2-6.3/books/tools/defconsts.lisp" "defconsts" "defconsts" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 985996327) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439))
1536662345