[acl2/acl2] eccd1f: [lists-light] Add some rules.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: eccd1f774325f10e687e50afadc0cdd85315a7e9
https://github.com/acl2/acl2/commit/eccd1f774325f10e687e50afadc0cdd85315a7e9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/lists-light/intersection-equal.lisp
M books/kestrel/lists-light/no-duplicatesp-equal.lisp
M books/kestrel/lists-light/remove1-equal.lisp

Log Message:
-----------
[lists-light] Add some rules.

Also make sure a rule about intersection-equal is in that book.


Commit: a9c1e05f1498827c69d83f498a7e6e434a1131dd
https://github.com/acl2/acl2/commit/a9c1e05f1498827c69d83f498a7e6e434a1131dd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/terms-light/arglistp1.lisp
M books/kestrel/terms-light/get-conjuncts.lisp
M books/kestrel/terms-light/logic-fnsp.lisp
M books/kestrel/terms-light/non-trivial-formals.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term-proofs.lisp

Log Message:
-----------
[terms-light] Add some rules.

And remove one now in lists-light.


Commit: b17917a040b3055372c1006b234aed32bd6ce757
https://github.com/acl2/acl2/commit/b17917a040b3055372c1006b234aed32bd6ce757
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)

Changed paths:
M Makefile
M axioms.lisp
M books/Makefile
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-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation-rules.lisp
M books/kestrel/remora/evaluation-tests.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking-tests.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names-validation.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp
M ld.lisp
M other-events.lisp

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


Commit: 1d7d68e9aa7345169b1b8db053a04ac9224c58a3
https://github.com/acl2/acl2/commit/1d7d68e9aa7345169b1b8db053a04ac9224c58a3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)

Changed paths:
M books/kestrel/c/atc/support/top.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.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/unique-names-validation.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.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

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


Commit: cef8b33069e4e02631e406163a76af8fe82adfda
https://github.com/acl2/acl2/commit/cef8b33069e4e02631e406163a76af8fe82adfda
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-23 (Thu, 23 Jul 2026)

Changed paths:
M axioms.lisp
M books/kestrel/arithmetic-light/minus.lisp
M books/kestrel/arithmetic-light/numerator.lisp
A books/kestrel/fty/symbol-set-set.lisp
M books/kestrel/fty/top.lisp
R books/kestrel/memory/acl2-customization.lsp
A books/kestrel/memory/make-memory-region-machinery.acl2
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.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/projects/abnf/notation/semantics.lisp
M books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp

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


Commit: 6d80b3911a5943eea4461fdcbe1cc49399dfa85b
https://github.com/acl2/acl2/commit/6d80b3911a5943eea4461fdcbe1cc49399dfa85b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-23 (Thu, 23 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/arithmetic.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/monomorphize.lisp
A books/kestrel/remora/omaps.lisp
R books/kestrel/remora/oset-omaps.lisp
A books/kestrel/remora/osets.lisp
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.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/std/util/definductive.lisp

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


Commit: 45c9bb6bdcc5aad2048b75c83b2d3ae13eabc187
https://github.com/acl2/acl2/commit/45c9bb6bdcc5aad2048b75c83b2d3ae13eabc187
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/array-declarators.c
A books/kestrel/c/transformation/tests/struct-type-split/array-index-effectful.c
A books/kestrel/c/transformation/tests/struct-type-split/array-init-designated.c
A books/kestrel/c/transformation/tests/struct-type-split/array-init-inferred-designated.c
A books/kestrel/c/transformation/tests/struct-type-split/array-init-positional.c
A books/kestrel/c/transformation/tests/struct-type-split/array-initializers.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member-flexible-after-anon.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member-flexible-nested-anon.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member-flexible.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member-sized-typedef.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member.c
A books/kestrel/c/transformation/tests/struct-type-split/array-vla-effectful.c
M books/kestrel/c/transformation/tests/struct-type-split/array.c
A books/kestrel/c/transformation/tests/struct-type-split/partial-init.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp

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


Commit: ce6074a2423bac5cce070099ef4aa95777646cc4
https://github.com/acl2/acl2/commit/ce6074a2423bac5cce070099ef4aa95777646cc4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp

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


Commit: 7b09d5b8663845b21395d5d1a496541c6aec12cd
https://github.com/acl2/acl2/commit/7b09d5b8663845b21395d5d1a496541c6aec12cd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treemap/doc.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/package.lsp
M books/kestrel/data/treemap/values.lisp
M books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/tree.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp
M books/kestrel/data/treeset/top.lisp
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.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/projects/fields/README
M books/projects/fields/embeddings.lisp
M books/projects/fields/extensions.lisp
M books/projects/fields/galois.lisp
A books/projects/fields/polynomials.lisp
M books/projects/fields/support/embeddings.lisp
M books/projects/fields/support/galois.lisp
A books/projects/fields/vectors.lisp
M books/projects/linear/field.lisp
M books/projects/linear/ring.lisp
M books/projects/linear/support/field.lisp
M books/projects/linear/support/ring.lisp
M books/projects/linear/support/vectors.lisp
M books/projects/linear/vectors.lisp
M books/std/util/definductive.lisp

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


Commit: 6709dd015c3064d844987ae50655d0187643b2cf
https://github.com/acl2/acl2/commit/6709dd015c3064d844987ae50655d0187643b2cf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M axioms.lisp
M books/demos/brr-free-variables-log.txt
M books/doc/relnotes.lisp
M books/kestrel/file-io-light/channels.lisp
M books/kestrel/file-io-light/close-output-channel.lisp
M books/kestrel/file-io-light/open-channels-p.lisp
M books/kestrel/file-io-light/read-byte-dollar.lisp
M books/kestrel/file-io-light/read-char-dollar.lisp
M books/kestrel/file-io-light/read-object.lisp
A books/kestrel/fty/set-list.lisp
M books/kestrel/fty/symbol-set-list-list.lisp
M books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
A books/kestrel/utilities/bind-to-bool.lisp
M books/kestrel/utilities/state.lisp
M books/kestrel/utilities/top.lisp
M books/std/io/base.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M books/system/update-state.lisp
M books/tools/with-supporters.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: b4fdaa8143c8db650b7772834a092bb1102773ba
https://github.com/acl2/acl2/commit/b4fdaa8143c8db650b7772834a092bb1102773ba
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/utilities/all-vars-in-term-bound-in-alistp.lisp
M books/kestrel/utilities/defopeners.lisp
M books/kestrel/utilities/terms.lisp

Log Message:
-----------
[utilities] Improve use of make-flag.


Commit: fcce54eef86a99f3335fe145012e59f5b636a6af
https://github.com/acl2/acl2/commit/fcce54eef86a99f3335fe145012e59f5b636a6af
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/axe/unify-term-and-dag-fast-correct.lisp
M books/kestrel/axe/unify-term-and-dag.lisp

Log Message:
-----------
[axe] Improve use of make-flag.


Commit: 49d8988bfaea4617c88df7fa488dfd72cf6509db
https://github.com/acl2/acl2/commit/49d8988bfaea4617c88df7fa488dfd72cf6509db
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/clause-processors/push-unary-fns-into-lambdas.lisp
M books/kestrel/clause-processors/push-unary-fns.lisp

Log Message:
-----------
[clause-processors] Improve use of make-flag.


Commit: fef9f8b828115862449e02a85888c119839c5ac8
https://github.com/acl2/acl2/commit/fef9f8b828115862449e02a85888c119839c5ac8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/evaluators/defevaluator-theorems.lisp

Log Message:
-----------
[evaluators] Improve use of make-flag.


Commit: 70d74aef89f710f55619b56f31b8addf393b701e
https://github.com/acl2/acl2/commit/70d74aef89f710f55619b56f31b8addf393b701e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/helpers/linter.lisp
M books/kestrel/helpers/model-induct.lisp

Log Message:
-----------
[helpers] Improve use of make-flag.


Commit: 0719f0d587f4178ba0671a07dd8ac7d5f61a7c7d
https://github.com/acl2/acl2/commit/0719f0d587f4178ba0671a07dd8ac7d5f61a7c7d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/terms-light/bound-vars-in-term.lisp
M books/kestrel/terms-light/combine-ifs-in-then-and-else-branches.lisp
M books/kestrel/terms-light/copy-term-proofs.lisp
M books/kestrel/terms-light/drop-trivial-lambdas-proofs.lisp
M books/kestrel/terms-light/drop-trivial-lambdas.lisp
M books/kestrel/terms-light/drop-unused-lambda-bindings-proofs.lisp
M books/kestrel/terms-light/drop-unused-lambda-bindings.lisp
M books/kestrel/terms-light/empty-eval-helpers.lisp
M books/kestrel/terms-light/expand-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/expand-lambdas-in-term.lisp
M books/kestrel/terms-light/free-vars-in-term.lisp
M books/kestrel/terms-light/function-call-subterms.lisp
M books/kestrel/terms-light/lambdas-closed-in-termp.lisp
M books/kestrel/terms-light/let-bind-formals-in-calls.lisp
M books/kestrel/terms-light/let-vars-in-term.lisp
M books/kestrel/terms-light/no-duplicate-lambda-formals-in-termp.lisp
M books/kestrel/terms-light/no-nils-in-termp.lisp
M books/kestrel/terms-light/reconstruct-lets-in-term-proofs.lisp
M books/kestrel/terms-light/reconstruct-lets-in-term.lisp
M books/kestrel/terms-light/rename-vars-in-term.lisp
M books/kestrel/terms-light/replace-term-with-term.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term.lisp
M books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
M books/kestrel/terms-light/simplify-ors-proofs.lisp
M books/kestrel/terms-light/simplify-ors.lisp
M books/kestrel/terms-light/sublis-var-and-magic-eval.lisp
M books/kestrel/terms-light/sublis-var-simple-proofs.lisp
M books/kestrel/terms-light/subst-var-alt-proofs.lisp
M books/kestrel/terms-light/subst-var-alt.lisp
M books/kestrel/terms-light/subst-var-deep.lisp
M books/kestrel/terms-light/substitute-constants-in-lambdas-proofs.lisp
M books/kestrel/terms-light/substitute-constants-in-lambdas.lisp
M books/kestrel/terms-light/substitute-lambda-formals.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars2-proofs.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars2.lisp
M books/kestrel/terms-light/termp-simple.lisp

Log Message:
-----------
[terms-light] Improve use of make-flag.


Commit: 78dcb9f9b968d613bf080549ea2fc65a39cf1a84
https://github.com/acl2/acl2/commit/78dcb9f9b968d613bf080549ea2fc65a39cf1a84
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/utilities/ld-history.lisp

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


Compare: https://github.com/acl2/acl2/compare/54521946294d...78dcb9f9b968

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