		Search-engine friendly clone of the ACL2 documentation.

Comp-stmt

Fixtype of compond-statements.

This is a product type introduced by fty::defprod.

Fields

labels — ident-list-list
items — block-item-list

As a GCC extension, we include lists of lists of identifiers at the beginning of compound statements. These represent sequences of label declarations: the outer list captures the sequence of declarations (nil if there are no label declarations), and each inner list captures the labels declared in the corresponding label declaration; currently we do not capture the restriction that each inner list must be non-empty.

Subtopics

Comp-stmtp: Recognizer for comp-stmt structures.
Comp-stmt-equiv: Basic equivalence relation for comp-stmt structures.
Make-comp-stmt: Basic constructor macro for comp-stmt structures.
Comp-stmt->labels: Get the labels field from a comp-stmt.
Change-comp-stmt: Modifying constructor for comp-stmt structures.
Comp-stmt->items: Get the items field from a comp-stmt.
Comp-stmt-fix: Fixing function for comp-stmt structures.
Comp-stmt-count: Measure for recurring over comp-stmt structures.