[acl2/acl2] d667a7: Paco: remove trailing blanks

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: d667a75006860f9e590c08b845a7be70b78ed84e
https://github.com/acl2/acl2/commit/d667a75006860f9e590c08b845a7be70b78ed84e
Author: nadezhin <Dmitry....@gmail.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/projects/paco/books/proveall.lsp
M books/projects/paco/database.lisp
M books/projects/paco/rewrite.lisp
M books/projects/paco/utilities.acl2

Log Message:
-----------
Paco: remove trailing blanks


Commit: ea532e3575811351c7cecdaeb618e5cb283fd2e2
https://github.com/acl2/acl2/commit/ea532e3575811351c7cecdaeb618e5cb283fd2e2
Author: nadezhin <Dmitry....@gmail.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/projects/paco/paco.lisp

Log Message:
-----------
Paco: fix name of the test file


Commit: fe40f691dfe86144a43dda1f22bad36b2098e4e5
https://github.com/acl2/acl2/commit/fe40f691dfe86144a43dda1f22bad36b2098e4e5
Author: nadezhin <Dmitry....@gmail.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/projects/paco/foundations.lisp

Log Message:
-----------
Paco: fix fn-count

fn-count mv-calls var-fn-count.
The names of results in this call were incorrect.
Fix it by swap of "var" and "fn".
Return values var and fn of mv-call of var-fn-count in the body


Commit: e902537a1dbca194979acbb883eff941c2f6fa4d
https://github.com/acl2/acl2/commit/e902537a1dbca194979acbb883eff941c2f6fa4d
Author: nadezhin <Dmitry....@gmail.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/projects/paco/foundations.lisp
M books/projects/paco/output-module.lisp

Log Message:
-----------
Fix wrong calls of fn-nume

First argument of fn-nume is a keyword, the second is a function names.
There were two calls where these arguments were swapped.


Commit: 8be1d20ff0ab1ba6f0419e4c9cb0c4c65063aefe
https://github.com/acl2/acl2/commit/8be1d20ff0ab1ba6f0419e4c9cb0c4c65063aefe
Author: nadezhin <Dmitry....@gmail.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/projects/paco/type-set.lisp

Log Message:
-----------
Paco: Use *ts-one* and *ts-integer>1* in type-set-XXXX functions

Definitions of *ts-one* and *ts-integer>* were alread ported from ACL2 to Paco,
but some type-set-XXX functions didn't use them.
Port remaining changes from ACL2.


Commit: 8b0c2e2884254101a29b80dd7ed6ec5990cce90a
https://github.com/acl2/acl2/commit/8b0c2e2884254101a29b80dd7ed6ec5990cce90a
Author: nadezhin <Dmitry....@gmail.com>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/projects/paco/induct.lisp
M books/projects/paco/prove.lisp
M books/projects/paco/rewrite.lisp
M books/projects/paco/simplify.lisp
M books/projects/paco/type-set.lisp

Log Message:
-----------
Paco: use o< instead of e0-ord-<

Use o< well-founded relation instead of e0-ord-< .
Disble unnecessary functions in measure proofs.
Remove speedup lemmas which becomes unnecessary.


Commit: ad76ceede4475969abae1339ab0655ded70bacab
https://github.com/acl2/acl2/commit/ad76ceede4475969abae1339ab0655ded70bacab
Author: MattKaufmann <kauf...@cs.utexas.edu>
Date: 2017-01-06 (Fri, 06 Jan 2017)

Changed paths:
M books/projects/paco/books/proveall.lsp
M books/projects/paco/database.lisp
M books/projects/paco/foundations.lisp
M books/projects/paco/induct.lisp
M books/projects/paco/output-module.lisp
M books/projects/paco/paco.lisp
M books/projects/paco/prove.lisp
M books/projects/paco/rewrite.lisp
M books/projects/paco/simplify.lisp
M books/projects/paco/type-set.lisp
M books/projects/paco/utilities.acl2

Log Message:
-----------
Merge pull request #680 from nadezhin/paco

Paco changes. (The type-set changes were probably not necessary, since they don't add to the educational value of Paco; but I checked with J and that's OK with him.) Thanks, Dima.


Compare: https://github.com/acl2/acl2/compare/5d26acc32431...ad76ceede447

[GitHub]

Branch: refs/heads/master