		Search-engine friendly clone of the ACL2 documentation.

Comm-asg

Make-comm-asg

Basic constructor macro for comm-asg structures.

Syntax

(make-comm-asg [:var <var>] 
               [:exp <exp>])

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

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

Definition

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

Macro: make-comm-asg

(defmacro make-comm-asg (&rest args)
  (std::make-aggregate 'comm-asg
                       args '((:var) (:exp))
                       'make-comm-asg
                       nil))

Function: comm-asg

(defun comm-asg (var exp)
  (declare (xargs :guard (and (stringp var) (aexpp exp))))
  (declare (xargs :guard t))
  (let ((__function__ 'comm-asg))
    (declare (ignorable __function__))
    (b* ((var (mbe :logic (str-fix var) :exec var))
         (exp (mbe :logic (aexp-fix exp) :exec exp)))
      (cons :asg (list var exp)))))