[acl2/acl2] 438cb0: [arithmetic-light] Add a rule.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 438cb04e0d20254b41edcd1b4cacfee10625edbd
https://github.com/acl2/acl2/commit/438cb04e0d20254b41edcd1b4cacfee10625edbd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)

Changed paths:
M books/kestrel/arithmetic-light/times.lisp

Log Message:
-----------
[arithmetic-light] Add a rule.


Commit: 9dbb0929caf2ab0762769218ff586ecdf35a6e98
https://github.com/acl2/acl2/commit/9dbb0929caf2ab0762769218ff586ecdf35a6e98
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)

Changed paths:
M books/kestrel/crypto/sha-3/sha-3.lisp

Log Message:
-----------
[sha-3] Clean up a bit.


Commit: cc0d7099c8b83229adbd795a3131b72fb04b6472
https://github.com/acl2/acl2/commit/cc0d7099c8b83229adbd795a3131b72fb04b6472
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/nat-lists.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/abnf/grammar-definer/top.lisp
M books/projects/abnf/grammar-parser/top.lisp
M books/projects/abnf/grammar-printer/top.lisp
M books/projects/abnf/notation/top.lisp
M books/projects/abnf/top.lisp

Log Message:
-----------
Merge.


Commit: 7bd22ea11267a1c7cafd6dde37eb0f3350f26249
https://github.com/acl2/acl2/commit/7bd22ea11267a1c7cafd6dde37eb0f3350f26249
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/rules.lisp

Log Message:
-----------
[bv] Move and improve a rule.


Commit: f64e8259ddf1cff4c37ce27e1d51222f6beae320
https://github.com/acl2/acl2/commit/f64e8259ddf1cff4c37ce27e1d51222f6beae320
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/leftrotate32.lisp
M books/kestrel/bv/sbvlt.lisp

Log Message:
-----------
[bv] Add a few rules.


Commit: e3f880256dea579e614190daeb8b0cb9f7ce62bb
https://github.com/acl2/acl2/commit/e3f880256dea579e614190daeb8b0cb9f7ce62bb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp

Log Message:
-----------
[axe] Reduce includes.


Commit: 7a67604db2bab0126221a24448d57e0825311978
https://github.com/acl2/acl2/commit/7a67604db2bab0126221a24448d57e0825311978
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp

Log Message:
-----------
[axe/arm] Add a rule.


Commit: 7a43e37e81c7ccc0122036ec6d888b808bbda381
https://github.com/acl2/acl2/commit/7a43e37e81c7ccc0122036ec6d888b808bbda381
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
A books/kestrel/terms-light/doc.acl2
A books/kestrel/terms-light/doc.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term-tests.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-tests.lisp
A books/kestrel/terms-light/simple-untranslate-in-term.lisp
M books/kestrel/terms-light/top.lisp
M books/kestrel/top-doc.lisp

Log Message:
-----------
Merge.


Commit: 02dfcd4bbd8b4ba009b1ac292c13b13238e4eadb
https://github.com/acl2/acl2/commit/02dfcd4bbd8b4ba009b1ac292c13b13238e4eadb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/kestrel/x86/alt-defs.lisp
M books/projects/abnf/notation/semantics.lisp
A books/projects/abnf/tree-operations/acl2-customization.lsp
A books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp

Log Message:
-----------
Merge.


Commit: 4871385bfdb0c63128669456876a5bf1b08e7973
https://github.com/acl2/acl2/commit/4871385bfdb0c63128669456876a5bf1b08e7973
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)

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

Log Message:
-----------
[axe] Keep rule disabled.


Compare: https://github.com/acl2/acl2/compare/f6f7eed604b6...4871385bfdb0

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

[Eric W. Smith]

Branch: refs/heads/master

[Eric W. Smith]

Branch: refs/heads/testing