		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-declon

Transform a declaration.

Signature
(simpadd0-declon declon gin) → (mv new-declon gout)
Arguments: declon — Guard (declonp declon).; gin — Guard (ginp gin).
Returns: new-declon — Type (declonp new-declon).; gout — Type (goutp gout).

In the case of a non-static-assert declaration, if a theorem was generated for the list of initializer declarators, it is regarded as the theorem for the declaration. This is so that the theorem can surface up to block item declarations.