[acl2/acl2] 43412d: [Remora] Add a structural op.

[Alessandro Coglio]

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

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp

Log Message:
-----------
[Remora] Add a structural op.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp

Log Message:
-----------
[Remora] Add a theorem.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp

Log Message:
-----------
[Remora] More surgical fixing.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp

Log Message:
-----------
[Remora] Add some theorems.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp

Log Message:
-----------
[Remora] More surgical fixings.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp

Log Message:
-----------
[Remora] Add some theorems.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp

Log Message:
-----------
[Remora] Add some doc.


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

Changed paths:
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
[Remora] Extend type equivalence for n-ary types.

Still some documented extensions needed.


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

Changed paths:
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation-tests.lisp

Log Message:
-----------
[Remora] Slightly improve some tests.


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

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Remove function no longer needed.


Commit: bca6c0f06837c49d32b08da727f2c464d41ea3b8
https://github.com/acl2/acl2/commit/bca6c0f06837c49d32b08da727f2c464d41ea3b8
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/projects/abnf/tree-operations/subtree-operations.lisp
M books/std/util/definductive.lisp

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


Compare: https://github.com/acl2/acl2/compare/9ba7ad2be4bb...bca6c0f06837

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

[Alessandro Coglio]

Branch: refs/heads/master

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

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...bca6c0f06837

[Alessandro Coglio]

Branch: refs/heads/testing