[acl2/acl2] c1e94b: [FTY] Add missing dash in `deffold-reduce`-generat...

[Alessandro Coglio]

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

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

Log Message:
-----------
[FTY] Add missing dash in `deffold-reduce`-generated theorems.


Commit: 47cb7d5569a2e7b36de5486c1f579e207ce4e50d
https://github.com/acl2/acl2/commit/47cb7d5569a2e7b36de5486c1f579e207ce4e50d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-07 (Sat, 07 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/unambiguity.lisp

Log Message:
-----------
[C$] Remove handwritten theorems now redundant.

This became apparent after fixing some names of theorems generated by
`deffold-reduce`.


Commit: a4efb776a9feb14c0c0554d64d6792d416a7693f
https://github.com/acl2/acl2/commit/a4efb776a9feb14c0c0554d64d6792d416a7693f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M bin/purity-acl2.sh
M books/GNUmakefile
M books/defexec/dag-unification/dag-unification-l.lisp
M books/defexec/dag-unification/dag-unification-rules.lisp
M books/defexec/dag-unification/dag-unification-st.lisp
M books/defexec/dag-unification/dags.lisp
M books/defexec/dag-unification/list-unification-rules.lisp
M books/defexec/dag-unification/matching.lisp
M books/defexec/dag-unification/subsumption-subst.lisp
M books/defexec/dag-unification/subsumption.lisp
M books/defexec/dag-unification/terms-as-dag.lisp
M books/defexec/dag-unification/terms-dag-stobj.lisp
M books/defexec/dag-unification/terms.lisp
M books/doc/practices.lisp
M books/doc/relnotes.lisp
M books/doc/top.lisp
M books/kestrel/air/model-0/air/pfcs-lifting.lisp
M books/kestrel/apt/doc.lisp
M books/kestrel/apt/isodata-doc.lisp
A books/kestrel/apt/simplify-conjunctions-tests.lisp
A books/kestrel/apt/simplify-conjunctions.lisp
M books/kestrel/apt/top.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
A books/kestrel/arm/rules.lisp
M books/kestrel/arm/top.lisp
M books/kestrel/axe/arm/examples/add/add-with-stop-pcs.lisp
M books/kestrel/axe/arm/examples/add/add.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/bv-list-rules-axe.lisp
M books/kestrel/axe/dag-conjuncts.lisp
M books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags2.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter-utilities3.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/prune-with-contexts-tests.lisp
M books/kestrel/axe/result-array-stobj.lisp
M books/kestrel/axe/rewriter-basic-tests.lisp
M books/kestrel/axe/rewriter-basic.lisp
M books/kestrel/axe/rewriter-tests.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/specialize.lisp
M books/kestrel/axe/strengthen-facts.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bitcoin/bech32.lisp
M books/kestrel/bv-lists/all-unsigned-byte-p2.lisp
M books/kestrel/bv-lists/append-arrays.lisp
M books/kestrel/bv-lists/bv-array-clear-range.lisp
M books/kestrel/bv-lists/bv-array-clear.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv-lists/bvchop-list.lisp
M books/kestrel/bv-lists/bvchop-list2.lisp
M books/kestrel/bv-lists/bvnot-list.lisp
M books/kestrel/bv-lists/logext-list.lisp
M books/kestrel/bv/.sys/in...@useless-runes.lsp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvlt-def.lisp
M books/kestrel/bv/bvsx-rules.lisp
M books/kestrel/bv/intro.lisp
M books/kestrel/bv/logand-b.lisp
M books/kestrel/bv/single-bit.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-binary-strict-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
A books/kestrel/c/examples/README.md
A books/kestrel/c/examples/add-uints.lisp
A books/kestrel/c/examples/add_uints.c
A books/kestrel/c/examples/cert.acl2
A books/kestrel/c/examples/strcpy-safe-support.lisp
A books/kestrel/c/examples/strcpy-safe.lisp
A books/kestrel/c/examples/strcpy_safe.c
M books/kestrel/c/language/keywords.lisp
A books/kestrel/c/proof-support/const-folding.lisp
M books/kestrel/c/proof-support/exec-stmt-openers.lisp
M books/kestrel/c/proof-support/top.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/abstract-syntax-structurals.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/abstract-syntax.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser-messages.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/positions.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-files.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/reader.lisp
A books/kestrel/c/syntax/spans.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
M books/kestrel/c/syntax/tests/reader.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/top.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/crypto/salsa/salsa20.lisp
M books/kestrel/error-checking/def-error-checker.lisp
M books/kestrel/risc-v/executable/decoding-executable.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/rflags-spec-sub.lisp
M books/kestrel/zcash/gadgets/a-3-3-1-alt-proof.lisp
M books/kestrel/zcash/gadgets/a-3-3-1-proof.lisp
M books/kestrel/zcash/gadgets/a-3-3-4-proof.lisp
A books/misc/character-encoding-test.acl2
M books/misc/character-encoding-test.lisp
M books/projects/acl2-in-hol/lisp/a2ml.bash
M books/projects/acl2-in-hol/lisp/axioms-essence.bash
M books/projects/acl2-in-hol/lisp/book-essence.bash
M books/projects/acl2-in-hol/tests/doit
M books/projects/acl2-in-hol/tests/inputs/Makefile
M books/projects/aleo/leo/early-version/definition/expressions.lisp
M books/projects/aleo/leo/early-version/definition/lexer.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/pfcs/.sys/parser-i...@useless-runes.lsp
M books/projects/pfcs/lifting.lisp
M books/projects/pfcs/parser-interface.lisp
M books/projects/pfcs/proof-support.lisp
M books/projects/pfcs/r1cs-bridge.lisp
M books/projects/pfcs/r1cs-subset.lisp
M books/projects/pfcs/semantics.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/set-theory/cantor.lisp
M books/std/system/remove-dead-if-branches.lisp
M books/system/doc/acl2-doc.lisp
M books/workshops/2000/medina/polynomials/polynomial.lisp
M books/workshops/2000/medina/polynomials/term.lisp
M books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp
M books/workshops/2000/ruiz/multiset/multiset.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/dags.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/terms.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp
M books/workshops/2004/ruiz-et-al/support/basic.lisp
M books/workshops/2004/ruiz-et-al/support/dag-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/dags.lisp
M books/workshops/2004/ruiz-et-al/support/matching.lisp
M books/workshops/2004/ruiz-et-al/support/prefix-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification-st.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification.lisp
M books/workshops/2004/ruiz-et-al/support/subsumption-subst.lisp
M books/workshops/2004/ruiz-et-al/support/subsumption.lisp
M books/workshops/2004/ruiz-et-al/support/terms-as-dag.lisp
M books/workshops/2004/ruiz-et-al/support/terms.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/coe-fld.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-producto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-suma.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuforma-normal.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fumonomio.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuopuesto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fusuma.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/futermino.lisp
M books/workshops/2007/cowles-et-al/support/greve/ack.lisp
M books/workshops/2007/cowles-et-al/support/greve/defminterm.lisp
M books/workshops/2007/cowles-et-al/support/greve/defxch.lisp
M books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp
M books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp
M books/workshops/2007/rubio/support/abstract-reductions/newman.lisp
M books/workshops/2007/rubio/support/multisets/multiset.lisp
M books/workshops/2007/rubio/support/simplicial-topology/generate-degenerate.lisp
M books/xdoc/save-classic.lisp
M books/xdoc/save-fancy.lisp
M books/xdoc/save-rendered.lisp
M books/xdoc/save.lisp
M books/xdoc/topics.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: 45086dd9a5f90db0004937922647bedf4bca1b75
https://github.com/acl2/acl2/commit/45086dd9a5f90db0004937922647bedf4bca1b75
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp
A books/kestrel/axe/arm/doc.acl2
A books/kestrel/axe/arm/doc.lisp
M books/kestrel/axe/doc.lisp

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


Commit: d6d9355595a46b8c18ceff69c1201cb4d1a2c35b
https://github.com/acl2/acl2/commit/d6d9355595a46b8c18ceff69c1201cb4d1a2c35b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

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

Log Message:
-----------
[FTY] Improve proofs generated by `deffold-reduce`.

Generate some enabled hints for the termination proofs.


Commit: 906477f5de3cd80f9f6333016a0f88cb1c2cd84a
https://github.com/acl2/acl2/commit/906477f5de3cd80f9f6333016a0f88cb1c2cd84a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/projects/pfcs/convenience-constructors.lisp
M books/projects/pfcs/package.lsp
M books/projects/pfcs/proof-support.lisp
M books/std/basic/top.lisp
A books/std/basic/yyyjoin.lisp

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


Compare: https://github.com/acl2/acl2/compare/640a7b1173d9...906477f5de3c

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