← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/std/lists/resize-list.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/resize-list.lisp
59
59
(defthm resize-list-when-atom
60
60
  (implies (atom lst)
61
61
           (equal (resize-list lst n default-value)
62
 
                  (replicate n default-value)))
63
 
  :hints(("Goal" :in-theory (enable replicate))))
 
62
                  (repeat n default-value)))
 
63
  :hints(("Goal" :in-theory (enable repeat))))
64
64
 
65
65
(local (defun my-induct (n m lst)
66
66
         (if (zp n)