[acl2/acl2] 9e6026: Prove that uniquify is identity if names already u...

[Stephen Westfold]

Branch: refs/heads/uniquify-identity
Home: https://github.com/acl2/acl2
Commit: 9e60261cbfc3b341c7d43c84c5b00546c69b02c1
https://github.com/acl2/acl2/commit/9e60261cbfc3b341c7d43c84c5b00546c69b02c1
Author: Stephen Westfold <west...@kestrel.edu>
Date: 2026-07-29 (Wed, 29 Jul 2026)

Changed paths:
A books/kestrel/lists-light/intersectp-equal.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/remora/osets.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/unique-names-validation.lisp
M books/kestrel/remora/unique-names.lisp

Log Message:
-----------
Prove that uniquify is identity if names already unique.

Add new lists-light book for intersectp-equal.
Disable tau where it is slow.



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