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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
; Tests of nesting 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
:check-expansion t))
(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-triple '(defun nest1 (x)
(cons x x)))))
; redundant
(my-make-event
'(my-make-event
(value-triple '(defun nest1 (x)
(cons x x)))))
; redundant
(my-make-event
'(make-event
(value-triple '(defun nest1 (x)
(cons x x)))))
(with-output
:off warning
(my-make-event
'(make-event
(value-triple '(with-output
:on warning
(defun nest2 (x)
(list x x)))))))
; redundant
(with-output
:off warning
(make-event
'(my-make-event
(value-triple '(with-output
:on event
(defun nest2 (x)
(list x x)))))))
; redundant
(with-output
:off warning
(my-make-event
'(my-make-event
(value-triple '(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))
:check-expansion t)))
(my-make-event
'(encapsulate
()
(my-make-event
'(defun test3 (x)
(cons x x)))))
(my-make-event
'(encapsulate
()
(make-event
'(defun test4 (x)
(cons x x)))))
(make-event
'(encapsulate
()
(my-make-event
'(defun test5 (x)
(cons x x)))))
|
