		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-init-declor

Transform an initializer declarator.

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

If a theorem was generated for the initializer, it is regarded as the theorem for the initializer declarator. This is so that the theorem can surface up to block item declarations.

If the type of the declared identifier is supported for proof generation, we update the variable-type map.