		Search-engine friendly clone of the ACL2 documentation.

Comm-if

Make-comm-if

Basic constructor macro for comm-if structures.

Syntax

(make-comm-if [:cond <cond>] 
              [:then <then>] 
              [:else <else>])

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

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

Definition

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

Macro: make-comm-if

(defmacro make-comm-if (&rest args)
  (std::make-aggregate 'comm-if
                       args '((:cond) (:then) (:else))
                       'make-comm-if
                       nil))

Function: comm-if

(defun comm-if (cond then else)
  (declare (xargs :guard (and (bexpp cond)
                              (comm-listp then)
                              (comm-listp else))))
  (declare (xargs :guard t))
  (let ((__function__ 'comm-if))
    (declare (ignorable __function__))
    (b* ((cond (mbe :logic (bexp-fix cond) :exec cond))
         (then (mbe :logic (comm-list-fix then)
                    :exec then))
         (else (mbe :logic (comm-list-fix else)
                    :exec else)))
      (cons :if (list cond then else)))))