[acl2/acl2] efbfc2: [ATC] Slightly improve generated limit terms.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: efbfc290fe21127cbbf727232eb4cbf8d6b6c2e4
https://github.com/acl2/acl2/commit/efbfc290fe21127cbbf727232eb4cbf8d6b6c2e4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-12 (Fri, 12 Dec 2025)

Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/statement-generation.lisp

Log Message:
-----------
[ATC] Slightly improve generated limit terms.

Use `+` instead of `binary-+`, which still satisfies `pseudo-termp`, although
the intention was for these to be translated terms. We should eventually move to
untranslated terms anyways, for better readability, and we should combine
constants.

Thanks to Eric Smith for suggesting this improvement.



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

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel