← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/misc/tailrec.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/centaur/misc/tailrec.lisp
714
714
     (equal (partial-ev (mk-list-term x) al)
715
715
            (partial-ev-lst x al)))
716
716
 
717
 
   (local
718
 
    (defthm take-len-when-true-listp
719
 
      (implies (and (true-listp x) (equal n (len x)))
720
 
               (equal (take n x)
721
 
                      x))))
722
 
 
723
717
   (defthm partial-ev-lst-type
724
718
     (true-listp (partial-ev-lst x al))
725
719
     :hints (("goal" :induct (len x)))