		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-init-declor-list

Transform a list of initializer declarators.

Signature
(simpadd0-init-declor-list initdeclors gin) → (mv new-initdeclors gout)
Arguments: initdeclors — Guard (init-declor-listp initdeclors).; gin — Guard (ginp gin).
Returns: new-initdeclors — Type (init-declor-listp new-initdeclors).; gout — Type (goutp gout).

If the list is a singleton and a theorem was generated for that one element, it is regarded as the theorem for the list of initializer declarators. This is so that the theorem can surface up to block item declarations.