		Search-engine friendly clone of the ACL2 documentation.

Dimb-amb-decl/stmt

Disambiguate an ambiguous declaration or statement.

Signature
(dimb-amb-decl/stmt decl/stmt table) → (mv erp decl-or-stmt new-table)
Arguments: decl/stmt — Guard (amb-decl/stmt-p decl/stmt).; table — Guard (dimb-tablep table).
Returns: erp — Type (maybe-msgp erp).; decl-or-stmt — Type (decl/stmt-p decl-or-stmt).; new-table — Type (dimb-tablep new-table).

An ambiguous declaration or statement is represented as a pair of a declaration and an expression (with the same concrete syntax appearance); the latter is an expression and not a statement because the statement in question is always an expression statement, and so it suffices to represent the expression. We attempt to disambiguate both the declaration and the expression, independently from each other. In valid code, one of them must succeed and the other one must fail: then we disambiguate in favor of the one that succeeded. If none or both succeed, the code must be invalid.