/usr/share/acl2-8.0dfsg/books/make-event/local-elided.lisp is in acl2-books-source 8.0dfsg-1.
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 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
;; [Jared and Sol]: we want to make sure this book gets provisionally certified
;; if we're doing any provisional certification, because
;; local-elided-include.lisp is going to test whether its .pcert0 file exists
;; as a proxy for checking whether it was provisionally or regularly certified,
;; and that's just sort of wrong...
(local (make-event '(defun foo (x) x)))
(make-event '(local (defun foo (x) x)))
(make-event '(local (defun foo-2 (x) x)))
(progn
(encapsulate
((bar1 (x) t))
(local (defun bar1 (x) (foo x)))
(defthm bar1-preserves-consp
(implies (consp x)
(consp (bar1 x))))))
(progn
(make-event '(local (defun g (x) x)))
(local (defun g2 (x) x))
(make-event
(value '(encapsulate
((bar2 (x) t))
(local (defun bar2 (x) (foo x)))
(defthm bar2-preserves-consp
(implies (consp x)
(consp (bar2 x))))))))
; redundant
(make-event
(value '(encapsulate
((bar2 (x) t))
(local (defun bar2 (x) (foo x)))
(defthm bar2-preserves-consp
(implies (consp x)
(consp (bar2 x)))))))
(make-event
(value '(encapsulate
((bar3 (x) t))
(make-event '(local (defun bar3 (x) (foo x))))
(defthm bar3-preserves-consp
(implies (consp x)
(consp (bar3 x)))))))
; redundant
(encapsulate
((bar3 (x) t))
(make-event '(local (defun bar3 (x) (foo x))))
(defthm bar3-preserves-consp
(implies (consp x)
(consp (bar3 x)))))
; Redundant after Version_7.1 (as of mid-September 2015).
(encapsulate
((bar3 (x) t))
(local (defun bar3 (x) (foo x)))
(defthm bar3-preserves-consp
(implies (consp x)
(consp (bar3 x)))))
(make-event '(defun foo-3 (x) x))
(defmacro my-local (x)
`(local ,x))
(encapsulate
()
(my-local (defun g3 (x) x))
(make-event '(my-local (defun g3 (x) x)))
(make-event '(my-local (defun g4 (x) x)))
(my-local (defun g4 (x) x))
(progn (my-local (defun g5 (x) x))
(my-local (make-event (value '(defun g6 (x) x))))))
|