Declaring a formal parameter name to be a single-threaded object
When a defun uses one of its formals as a single-threaded
object (stobj), the
If the formal in question is
or, more generally,
where all the single-threaded formals are listed.
For such a declaration to be legal it must be the case that all the names have previously been defined as single-threaded objects with defstobj.
When an argument is declared to be single-threaded the guard of the function is augmented by conjoining to it the condition that the argument satisfy the recognizer for the single-threaded object. Furthermore, the syntactic checks done to enforce the legal use of single-threaded objects are also sufficient to allow these guard conjuncts to be automatically proved.
The obvious question arises: Why does ACL2 insist that you declare stobj
names before using them in
Suppose that one user, say Jones, creates a book in which
ACL2 insists on the declaration to ensure that the definition is processed the same way no matter what the context.