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