		Search-engine friendly clone of the ACL2 documentation.

Jstatem-do

Make-jstatem-do

Basic constructor macro for jstatem-do structures.

Syntax

(make-jstatem-do [:body <body>] 
                 [:test <test>])

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

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

Definition

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

Macro: make-jstatem-do

(defmacro make-jstatem-do (&rest args)
  (std::make-aggregate 'jstatem-do
                       args '((:body) (:test))
                       'make-jstatem-do
                       nil))

Function: jstatem-do

(defun jstatem-do (body test)
  (declare (xargs :guard (and (jblockp body) (jexprp test))))
  (declare (xargs :guard t))
  (let ((__function__ 'jstatem-do))
    (declare (ignorable __function__))
    (b* ((body (mbe :logic (jblock-fix body)
                    :exec body))
         (test (mbe :logic (jexpr-fix test)
                    :exec test)))
      (cons :do (list body test)))))