/usr/share/acl2-7.2dfsg/books/make-event/basic-check.lisp is in acl2-books-source 7.2dfsg-3.
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 | ; 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.
; This variant of basic.lisp uses :check-expansion t. If you care to look in
; basic-check.cert, you'll see that the expansions saved for test1 (position 1
; in this file) and test2 (position 2 in this file) are of the form
; (record-expansion original-form new-form), where original-form is as below
; and new-form is similar but with the :check-expansion filled in with the
; result of expanding the argument of make-event.
(in-package "ACL2")
; Here's something fun to try interactively.
#|
(make-event
(er-progn (assign saved-len (length (w state)))
(value '(value-triple nil))))
; Defines (foo x) to be x.
(make-event
(if (equal (length (w state)) (@ saved-len))
'(defun foo (x) x)
'(defun foo (x) (cons x x))))
:pe foo
; Causes a redefinition error.
(make-event
(if (equal (length (w state)) (@ saved-len))
'(defun foo (x) x)
'(defun foo (x) (cons x x))))
; Works but defines (bar x) to be (cons x x).
(make-event
(if (equal (length (w state)) (@ saved-len))
'(defun bar (x) x)
'(defun bar (x) (cons x x))))
:ubt 1
; This time (bar x) is x.
(make-event
(if (equal (length (w state)) (@ saved-len))
'(defun bar (x) x)
'(defun bar (x) (cons x x))))
|# ; |
(make-event
'(defun test1 (x)
(cons x x))
:check-expansion t)
(make-event
(value '(defun test2 (x)
(cons x x)))
:check-expansion t)
(defun bar (x)
(cons (test1 x) (test2 x)))
(defthm bar-prop
(equal (bar x)
(cons (cons x x)
(cons x x))))
|