		Search-engine friendly clone of the ACL2 documentation.

Memory

Private

Redundantly define, then serverely restrict the usage of some function.

Example:

(private foo (x y)
   (if (atom x)
       ...))

private is a macro which may be useful for authors of libraries, or to users who want to enforce severe discipline upon themselves.

The macro is similar to defund in that it first introduces a defun and then immediately disables its definition. However, private goes further: it also disables the resulting type-prescription rule and sets up theory-invariants that prohibit the user from ever enabling the definition or the type prescription.

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 private, you can identify functions that you want to keep control over and that the user should either (1) not be using at all, or (2) only be reasoning about using the theorems your have provided.

To use private, simply copy your (defun foo ...) form into your interface file, then replace defun with private.