/usr/share/acl2-6.3/books/tools/fake-event.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (LOCAL (PROGN (DEFUN TEST-FAKE-EVENT (N STATE) (DECLARE (XARGS :MODE :PROGRAM :STOBJS STATE)) (IF (ZP N) (MV 0 STATE) (MV-LET (RAND STATE) (RANDOM$ 10 STATE) (MV-LET (ERP VAL STATE) (FAKE-EVENT (CONS (QUOTE WITH-OUTPUT) (CONS (QUOTE :OFF) (CONS (QUOTE :ALL) (CONS (CONS (QUOTE MAKE-EVENT) (CONS (CONS (QUOTE QUOTE) (CONS (CONS (QUOTE DEFTHM) (CONS (QUOTE FOO) (CONS (CONS (QUOTE MEMBER) (CONS RAND (CONS (CONS (QUOTE QUOTE) (CONS (CONS (QUOTE 0) (CONS (QUOTE 1) (CONS (QUOTE 5) (CONS (QUOTE 7) (QUOTE NIL))))) (QUOTE NIL))) (QUOTE NIL)))) (CONS (QUOTE :RULE-CLASSES) (CONS (QUOTE NIL) (QUOTE NIL)))))) (QUOTE NIL))) (QUOTE NIL))) (QUOTE NIL)))))) (DECLARE (IGNORE VAL)) (MV-LET (REST STATE) (TEST-FAKE-EVENT (1- N) STATE) (MV (+ REST (IF ERP 0 1)) STATE)))))) (MAKE-EVENT (MV-LET (N STATE) (TEST-FAKE-EVENT 20 STATE) (IF (> N 10) (VALUE (QUOTE (VALUE-TRIPLE :MORE))) (VALUE (QUOTE (VALUE-TRIPLE :LESS)))))))) (LOCAL (VALUE-TRIPLE :ELIDED))))
NIL
(("/usr/share/acl2-6.3/books/tools/fake-event.lisp" "fake-event" "fake-event" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 874792716))
722568559
|