		Search-engine friendly clone of the ACL2 documentation.

Vl-stmt

Vl-whilestmt

Representation of while statements.

This is a product type, introduced by deftagsum in support of vl-stmt.

Fields

condition — vl-expr
body — vl-stmt
atts — vl-atts

General Form:

while (<condition>)
   <body>

See Section 9.6 (page 130). The semantics are like those of while loops in C; body is executed until condition becomes false. If condition is false to begin with, then body is not executed at all.

Subtopics

Vl-whilestmt->condition: Get the condition field from a vl-whilestmt.
Make-vl-whilestmt: Basic constructor macro for vl-whilestmt structures.
Vl-whilestmt->body: Get the body field from a vl-whilestmt.
Vl-whilestmt->atts: Get the atts field from a vl-whilestmt.
Change-vl-whilestmt: Modifying constructor for vl-whilestmt structures.