[acl2/acl2] a3d6de: [definductive] Generalize some code.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: a3d6de0dfc2eb075993c30935658e9503e1a3299
https://github.com/acl2/acl2/commit/a3d6de0dfc2eb075993c30935658e9503e1a3299
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/std/util/definductive.lisp

Log Message:
-----------
[definductive] Generalize some code.

This is for proof validity checking functions for mutually recursive
proofs/predicates.


Commit: 3957e9d4057b4a647adc463760ef3521fb5d3956
https://github.com/acl2/acl2/commit/3957e9d4057b4a647adc463760ef3521fb5d3956
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/std/util/definductive.lisp

Log Message:
-----------
[definductive] Consolidate two functions.


Commit: d23496528da395862ad9b63257c2227371ec1926
https://github.com/acl2/acl2/commit/d23496528da395862ad9b63257c2227371ec1926
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/std/util/definductive.lisp

Log Message:
-----------
[definductive] Streamline a proof.


Commit: 9ba7ad2be4bbcf3263472548ec7a2252637253cd
https://github.com/acl2/acl2/commit/9ba7ad2be4bbcf3263472548ec7a2252637253cd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/rules3.lisp
R books/kestrel/bv/.sys/ru...@useless-runes.lsp
M books/kestrel/bv/rules.lisp
M books/kestrel/c/atc/abstract-syntax.lisp
M books/kestrel/c/atc/tutorial.lisp
M books/kestrel/c/language/abstract-syntax.lisp
M books/kestrel/c/language/implementation-environments/char-formats.lisp
M books/kestrel/c/language/implementation-environments/integer-format-templates.lisp
M books/kestrel/c/language/implementation-environments/integer-formats.lisp
M books/kestrel/c/language/implementation-environments/schar-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
M books/kestrel/c/language/implementation-environments/uchar-formats.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
A books/kestrel/c/syntax/preprocessing-abstract-syntax.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
R books/kestrel/c/syntax/preprocessor-files.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/transformation/json-rpc/struct-type-split.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
M books/kestrel/file-io-light/open-output-channel.lisp
M books/kestrel/file-io-light/read-bytes-from-channel.lisp
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
R books/kestrel/remora/abstract-syntax-well-formed.lisp
A books/kestrel/remora/abstract-syntax-well-formedness.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/check-keywords.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation-rules.lisp
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/printer.lisp
M books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/filesystems/utilities/cpp-syntax/package.lsp

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


Compare: https://github.com/acl2/acl2/compare/8f87a5c30b21...9ba7ad2be4bb

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