← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/std/util/tests/defalist.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/std/util/tests/defalist.lisp
160
160
                  :valp-of-nil nil))))
161
161
 
162
162
 
 
163
 
 
164
(local (encapsulate ()
 
165
         (local (defalist no-key (x)
 
166
                  :val (integerp x)
 
167
                  :valp-of-nil nil))))
 
168
 
 
169
 
 
170
(local (encapsulate ()
 
171
         (local (defalist no-val (x)
 
172
                  :key (integer-listp x)
 
173
                  :keyp-of-nil t))))
 
174
 
163
175
;; check for special trivial sorts of things that ACL2 can rewrite in deep
164
176
;; ways.  this has screwed us up before due to restrictions on :rewrite rules,
165
177
;; etc.
214
226
 
215
227
 
216
228
 
 
229
 
 
230
 
217
231
(local (progn
218
232
 
219
233
(defalist m0 (x)
284
298
         (my-alistp (cdr x)))))
285
299
 
286
300
(defthm my-alistp-when-not-consp
287
 
  (implies (not (consp x))
288
 
           (equal (my-alistp x)
289
 
                  (not x))))
 
301
  (implies (not (consp acl2::x))
 
302
           (equal (my-alistp acl2::x)
 
303
                  (not acl2::x))))
290
304
 
291
305
(defthm my-alistp-of-cons
292
 
  (equal (my-alistp (cons a x))
293
 
         (and (consp a)
294
 
              (stringp (car a))
295
 
              (maybe-natp (cdr a))
296
 
              (my-alistp x))))
 
306
  (equal (my-alistp (cons acl2::a acl2::x))
 
307
         (and (and (consp acl2::a)
 
308
                   (stringp (car acl2::a))
 
309
                   (maybe-natp (cdr acl2::a)))
 
310
              (my-alistp acl2::x))))
297
311
 
298
312
(defalist my-alistp (x)
299
313
  :key (stringp x)
301
315
  :keyp-of-nil nil
302
316
  :valp-of-nil t
303
317
  :already-definedp t
304
 
  :true-listp t)
 
318
  :true-listp t
 
319
  :theory-hack ((local (in-theory (enable maybe-natp)))))
305
320
 
306
 
))
 
 
b'\\ No newline at end of file'
 
321
))