		Search-engine friendly clone of the ACL2 documentation.

Stmt-gotoe

Make-stmt-gotoe

Basic constructor macro for stmt-gotoe structures.

Syntax

(make-stmt-gotoe [:label <label>])

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

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

Definition

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

Macro: make-stmt-gotoe

(defmacro make-stmt-gotoe (&rest args)
  (std::make-aggregate 'stmt-gotoe
                       args '((:label))
                       'make-stmt-gotoe
                       nil))

Function: stmt-gotoe

(defun stmt-gotoe (label)
  (declare (xargs :guard (exprp label)))
  (declare (xargs :guard t))
  (b* ((label (mbe :logic (expr-fix label)
                   :exec label)))
    (cons :gotoe label)))