		Search-engine friendly clone of the ACL2 documentation.

Valid-initer-option

Validate an optional initializer.

Signature
(valid-initer-option initer? target-type lifetime? table ienv) → (mv erp new-initer? return-types new-table)
Arguments: initer? — Guard (initer-optionp initer?).; target-type — Guard (typep target-type).; lifetime? — Guard (lifetime-optionp lifetime?).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-initer? — Type (initer-optionp new-initer?).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

If there is no initializer, validation succeeds. Otherwise, we validate the initializer.

The guard on the target type is weakened, compared to valid-initer: if there is no initializer, the type can be anything, because the restriction applies only to initializers [C17:6.7.9/3].