[acl2/acl2] 83dacc: [arithmetic-light] Add 2 rules.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 83dacca7c5b375fb4ea1c774f8d80c0742e8596c
https://github.com/acl2/acl2/commit/83dacca7c5b375fb4ea1c774f8d80c0742e8596c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp

Log Message:
-----------
[arithmetic-light] Add 2 rules.


Commit: e361b2cbde30cd2bc2bfc1d361043966549d13bb
https://github.com/acl2/acl2/commit/e361b2cbde30cd2bc2bfc1d361043966549d13bb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp

Log Message:
-----------
[bv-lists/axe] Add more rules to shorten arrays.


Commit: e1fd756d462cd588bcb3ab5f7bc80d31da045466
https://github.com/acl2/acl2/commit/e1fd756d462cd588bcb3ab5f7bc80d31da045466
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/bv/bvlt.lisp

Log Message:
-----------
[bv] Organize rules.


Commit: 22cc9f8fa90c8f58603d4390585b0a01921ff5bd
https://github.com/acl2/acl2/commit/22cc9f8fa90c8f58603d4390585b0a01921ff5bd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/rules3.lisp

Log Message:
-----------
[axe] Add todo.


Compare: https://github.com/acl2/acl2/compare/a313551efed3...22cc9f8fa90c

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/master

Commit: 291f9dee9dfe61322f8117ddd9f7b13f2ed69fbe
https://github.com/acl2/acl2/commit/291f9dee9dfe61322f8117ddd9f7b13f2ed69fbe
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp

M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp

M books/kestrel/bv/bvlt.lisp

Log Message:
-----------

Merge commit '22cc9f8fa90c8f58603d4390585b0a01921ff5bd' into HEAD


Compare: https://github.com/acl2/acl2/compare/e1ac360f5950...291f9dee9dfe

[acl2buildserver]

Branch: refs/heads/testing