[acl2/acl2] 9518fd: [deffold-map] Make guard proofs more robust.

[Alessandro Coglio]

Branch: refs/heads/deffold-map
Home: https://github.com/acl2/acl2
Commit: 9518fd8b0aed937694b646353076bb9cead4f924
https://github.com/acl2/acl2/commit/9518fd8b0aed937694b646353076bb9cead4f924
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-11 (Tue, 11 Aug 2026)

Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------
[deffold-map] Make guard proofs more robust.



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

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

Home: https://github.com/acl2/acl2
Commit: 9518fd8b0aed937694b646353076bb9cead4f924
https://github.com/acl2/acl2/commit/9518fd8b0aed937694b646353076bb9cead4f924
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-11 (Tue, 11 Aug 2026)

Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------
[deffold-map] Make guard proofs more robust.

Commit: 3510c0dfb98927b746a2d681129c1aa016185072
https://github.com/acl2/acl2/commit/3510c0dfb98927b746a2d681129c1aa016185072
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bvcat.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/eval-from-file.lisp
M books/kestrel/remora/evaluation-tests.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/monomorphize-from-file.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/osets.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-equivalence.lisp
A books/kestrel/remora/unique-names-properties.lisp
M books/kestrel/remora/utility-transforms.lisp
A books/kestrel/remora/well-formedness-under-desugaring.lisp
M books/kestrel/utilities/translate.lisp

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


Commit: a1e9e2a450a93b2a34068891fc6756a84ad92466
https://github.com/acl2/acl2/commit/a1e9e2a450a93b2a34068891fc6756a84ad92466
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:

M books/kestrel/fty/deffold-map.lisp

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

[deffold-map] Fix some doc as suggested by GJ.


Commit: cec9912268dbd2f7cf2bab1dbf0b1da1575886dc
https://github.com/acl2/acl2/commit/cec9912268dbd2f7cf2bab1dbf0b1da1575886dc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:

M books/kestrel/fty/deffold-map.lisp

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

[deffold-map] Fix/improve some doc.

Based on some feedback from Grant Jurgensen.


Commit: 7a31c78f91fc4d54f5037e34aa2c4cf49556bf0e
https://github.com/acl2/acl2/commit/7a31c78f91fc4d54f5037e34aa2c4cf49556bf0e
Author: Alessandro Coglio <2409151...@users.noreply.github.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp

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

Merge pull request #2011 from acl2/deffold-map

[deffold-map] Make guard proofs more robust.

Compare: https://github.com/acl2/acl2/compare/96665c3f9704...7a31c78f91fc

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing