Redundantly define, then serverely restrict the usage of some function.
The macro is similar to defund in that it first introduces a defun
and then immediately disables its definition. However,
Why would we want such a thing? A nice way to develop libraries is to use ACL2::redundant-events in an interface file, so that users never even see the local lemmas and so forth that you used to get the proofs to go through. This gives you the freedom to change and remove those definitions at will.
Unfortunately, you cannot do the same for functions, because ACL2 needs the
functions available in the interface book if they are ever used. With
To use private, simply copy your