		Search-engine friendly clone of the ACL2 documentation.

Statement-assign-single

Make-statement-assign-single

Basic constructor macro for statement-assign-single structures.

Syntax

(make-statement-assign-single [:target <target>] 
                              [:value <value>])

This is the usual way to construct statement-assign-single structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-statement-assign-single

(defmacro make-statement-assign-single (&rest args)
  (std::make-aggregate 'statement-assign-single
                       args '((:target) (:value))
                       'make-statement-assign-single
                       nil))

Function: statement-assign-single

(defun statement-assign-single (target value)
  (declare (xargs :guard (and (pathp target)
                              (expressionp value))))
  (declare (xargs :guard t))
  (let ((__function__ 'statement-assign-single))
    (declare (ignorable __function__))
    (b* ((target (mbe :logic (path-fix target)
                      :exec target))
         (value (mbe :logic (expression-fix value)
                     :exec value)))
      (cons :assign-single (list target value)))))