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
|
; 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.
; Here are some tests for nesting of make-event forms: macros, local,
; skip-proofs, with-output, and recursive make-event.
(in-package "ACL2")
(defmacro my-make-event (&rest args)
`(make-event ,@args))
(my-make-event
'(my-make-event
'(defun nest1 (x)
(cons x x))))
(defthm nest1-prop
(equal (nest1 x)
(cons x x)))
; redundant
(make-event
'(my-make-event
(value '(defun nest1 (x)
(cons x x)))))
; redundant
(my-make-event
'(make-event
(value '(defun nest1 (x)
(cons x x)))))
(with-output
:off warning
(my-make-event
'(make-event
(value '(with-output
:on warning
(defun nest2 (x)
(list x x)))))))
; redundant
(with-output
:off warning
(make-event
'(my-make-event
(value '(with-output
:on event
(defun nest2 (x)
(list x x)))))))
; nested redundant event
(encapsulate
()
(my-make-event
'(defun nest1 (x)
(cons x x)))
(defun bar (x) x))
; encapsulate and make-event
(make-event
'(encapsulate
()
(make-event
'(defun test2 (x)
(cons x x)))))
|
