Improved the copy-def utility.

Quoting :doc note-8-1-books: Improved the copy-def utility (community book kestrel/utilities/copy-def.lisp) by adding an :expand hint in the recursive case, as is sometimes necessary.
acl2 · Jan 11, 2018 · 5366414 · 5366414
1 parent 4ae5f6b
commit 5366414
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/books/doc/relnotes.lisp b/books/doc/relnotes.lisp
@@ -117,6 +117,10 @@
  <p>Added a <see topic='@(url fty)'>fixtype</see>
  for <see topic='@(url set::std/osets)'>finite sets</see>.</p>
 
+ <p>Improved the @('copy-def') utility (community book
+ @('kestrel/utilities/copy-def.lisp')) by adding an @(':expand') hint in the
+ recursive case, as is sometimes necessary.</p>
+
  <h4><see topic='@(url soft::soft)'>SOFT</see></h4>
 
  <p>Added a @(':print') option to control screen output.</p>

diff --git a/books/kestrel/utilities/copy-def.lisp b/books/kestrel/utilities/copy-def.lisp
@@ -175,7 +175,8 @@
        ,@(and (eq flagp nil)
               `(:hints
                 (("Goal"
-                  ,@(and singly-recursivep `(:induct ,fn-call)))
+                  ,@(and singly-recursivep `(:induct ,fn-call))
+                  :expand (,fn-call ,fn-copy-call))
                  ,@(and hyps-preserved-thm-names
                         `('(:use (,@hyps-preserved-thm-names)))))))
        ,@(and (eq flagp t)