|
|
|---|
|
|
|
|---|
(any-p x) is always true; i.e., it recognizes any ACL2 object.
This is a ``degenerate'' recognizer which is sometimes useful for fty. For instance, it allows you to have fields within a fty::defprod that are completely unconstrained, which may be especially useful when you are in the early stages of development and haven't yet thought much about types.
Function:
(defun any-p$inline (x) (declare (xargs :guard t) (ignore x)) t)