← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/std/lists/reverse.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/lists/reverse.lisp
62
62
    (equal (true-listp (reverse x))
63
63
           (not (stringp x))))
64
64
 
65
 
  ;; ACL2's built-in type-prescription rule is weaker than it should be:
66
 
  ;;
67
 
  ;; (OR (CONSP (REVERSE X))
68
 
  ;;     (EQUAL (REVERSE X) NIL)
69
 
  ;;     (STRINGP (REVERSE X)))
70
 
  ;;
71
 
  ;; So let's install a better one...
72
 
 
73
 
  (in-theory (disable (:type-prescription reverse)))
74
 
 
75
 
  (defthm reverse-type
76
 
    (or (stringp (reverse x))
77
 
        (true-listp (reverse x)))
78
 
    :rule-classes :type-prescription)
79
 
 
80
65
  (local (defthm len-zero
81
66
           (equal (equal 0 (len x))
82
67
                  (atom x))))