		Search-engine friendly clone of the ACL2 documentation.

Stmt-dowhile

Make-stmt-dowhile

Basic constructor macro for stmt-dowhile structures.

Syntax

(make-stmt-dowhile [:body <body>] 
                   [:test <test>])

This is the usual way to construct stmt-dowhile structures. It simply conses together a structure with the specified fields.

This macro generates a new stmt-dowhile structure from scratch. See also change-stmt-dowhile, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-stmt-dowhile

(defmacro make-stmt-dowhile (&rest args)
  (std::make-aggregate 'stmt-dowhile
                       args '((:body) (:test))
                       'make-stmt-dowhile
                       nil))

Function: stmt-dowhile

(defun stmt-dowhile (body test)
  (declare (xargs :guard (and (stmtp body) (exprp test))))
  (declare (xargs :guard t))
  (let ((__function__ 'stmt-dowhile))
    (declare (ignorable __function__))
    (b* ((body (mbe :logic (stmt-fix body) :exec body))
         (test (mbe :logic (expr-fix test)
                    :exec test)))
      (cons :dowhile (list body test)))))