[acl2/acl2] 24b69e: Improve redundancy handling of APT transformations...

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 24b69e4884a60a7fc675a4022e97f83b7c8f2337
https://github.com/acl2/acl2/commit/24b69e4884a60a7fc675a4022e97f83b7c8f2337
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-06 (Sun, 06 Aug 2017)

Changed paths:
M books/kestrel/apt/package.lsp
M books/kestrel/apt/restrict-tests.lisp
M books/kestrel/apt/restrict.lisp
M books/kestrel/apt/tailrec-tests.lisp
M books/kestrel/apt/tailrec.lisp

Log Message:
-----------
Improve redundancy handling of APT transformations.

Now the :VERBOSE and :SHOW-ONLY option, which only affect screen output, do not
affect redundancy checks.

When a transformation is redundant and :SHOW-ONLY is T, the ENCAPSULATE
(retrieved from the transformation table) is shown on screen.

Instead of :REDUNDANT, a phrase is shown on screen if a transformaion is
redundant.

[GitHub]

Branch: refs/heads/master