		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-param-declor

Transform a parameter declarator.

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

If the type of the parameter declarator is in the subset supported by our formal semantics, we extend the variable-type map with the parameter and its type.