		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Stmt-formalp

Check if a statement has formal dynamic semantics.

Signature
(stmt-formalp stmt) → yes/no
Arguments: stmt — Guard (stmtp stmt).
Returns: yes/no — Type (booleanp yes/no).

Statements not supported by ldm-stmt are not supported here either. In addition, we look at c::exec-stmt to determine which of those statements have formal dynamic semantics, and what restrictions there are on the kinds of expressions that can occur in the statements.