[acl2/acl2] 7128d4: [treeset] Add generic count.

[Grant Jurgensen]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 7128d48b2c296458d72f973efc3122546775e9c4
https://github.com/acl2/acl2/commit/7128d48b2c296458d72f973efc3122546775e9c4
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
A books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/top.lisp

Log Message:
-----------
[treeset] Add generic count.


Commit: d6e01c7b04abd12b986c06ffae2754eb0996edc9
https://github.com/acl2/acl2/commit/d6e01c7b04abd12b986c06ffae2754eb0996edc9
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treeset/defs.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/top.lisp

Log Message:
-----------
[treeset] Add generic iterator recognizer.


Commit: a5577b499ce4c18767c48abc3a6ddb610d9bd0c5
https://github.com/acl2/acl2/commit/a5577b499ce4c18767c48abc3a6ddb610d9bd0c5
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treemap/doc.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/package.lsp
M books/kestrel/data/treemap/values.lisp
M books/kestrel/data/treeset/package.lsp

Log Message:
-----------
[data] Home treeset/treemap xdoc topics in the ACL2 package.

Import the package-name symbols so the top-level topics are acl2::treeset and acl2::treemap, matching how cross-package references (e.g. from treemap) link to them.


Commit: 312a4518c97c2f94c98a0a22c7763bcea087776a
https://github.com/acl2/acl2/commit/312a4518c97c2f94c98a0a22c7763bcea087776a
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treeset/internal/tree.lisp

Log Message:
-----------
[treeset] Add acl2-count bound for tree element values.

A linear rule giving acl2-count(tree-element->val elem) <= acl2-count(elem), carrying the element-of-node measure edge for structural recursion through tree elements (e.g. mutually recursive FTY treeset cliques).


Commit: 6d7422df898c77731011eb5bb96c7476a539acf6
https://github.com/acl2/acl2/commit/6d7422df898c77731011eb5bb96c7476a539acf6
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treeset/generic-count.lisp

Log Message:
-----------
[treeset] Simplify generic count book.


Compare: https://github.com/acl2/acl2/compare/ee340914c66f...6d7422df898c

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

[acl2buildserver]

Branch: refs/heads/master

Commit: 7d2ed67b4a94b6ab03cceff63171aae7dff75b96
https://github.com/acl2/acl2/commit/7d2ed67b4a94b6ab03cceff63171aae7dff75b96
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treemap/doc.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/package.lsp
M books/kestrel/data/treemap/values.lisp

M books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/tree.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp

M books/kestrel/data/treeset/top.lisp

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

Merge commit '6d7422df898c77731011eb5bb96c7476a539acf6' into HEAD


Compare: https://github.com/acl2/acl2/compare/1ec2dac601ef...7d2ed67b4a94

[acl2buildserver]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Commit: 1ec2dac601ef8b6ef0ca8852085d402bc8ad38bd
https://github.com/acl2/acl2/commit/1ec2dac601ef8b6ef0ca8852085d402bc8ad38bd
Author: Matt Kaufmann <kauf...@cs.utexas.edu>

Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:

M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt

Log Message:
-----------
Clarified in :DOC defttag that there is at most one active ttag at a time.

Thanks to Eric Smith for suggestion that such a clarification could be
useful.

Commit: 7d2ed67b4a94b6ab03cceff63171aae7dff75b96
https://github.com/acl2/acl2/commit/7d2ed67b4a94b6ab03cceff63171aae7dff75b96
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treemap/doc.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/package.lsp
M books/kestrel/data/treemap/values.lisp
M books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/tree.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp
M books/kestrel/data/treeset/top.lisp

Log Message:
-----------
Merge commit '6d7422df898c77731011eb5bb96c7476a539acf6' into HEAD

Commit: d3d18802f2c5f837a70135a415c56db73a72b28f
https://github.com/acl2/acl2/commit/d3d18802f2c5f837a70135a415c56db73a72b28f
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treemap/doc.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/package.lsp
M books/kestrel/data/treemap/values.lisp
M books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/tree.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp
M books/kestrel/data/treeset/top.lisp

M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt

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


Compare: https://github.com/acl2/acl2/compare/dccf8aee3d73...d3d18802f2c5