		Search-engine friendly clone of the ACL2 documentation.

Statement-if

Make-statement-if

Basic constructor macro for statement-if structures.

Syntax

(make-statement-if [:branches <branches>] 
                   [:else <else>])

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

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

Definition

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

Macro: make-statement-if

(defmacro make-statement-if (&rest args)
  (std::make-aggregate 'statement-if
                       args '((:branches) (:else))
                       'make-statement-if
                       nil))

Function: statement-if

(defun statement-if (branches else)
  (declare (xargs :guard (and (branch-listp branches)
                              (statement-listp else))))
  (declare (xargs :guard (consp branches)))
  (let ((__function__ 'statement-if))
    (declare (ignorable __function__))
    (b* ((branches (mbe :logic (branch-list-fix branches)
                        :exec branches))
         (else (mbe :logic (statement-list-fix else)
                    :exec else)))
      (let ((branches (mbe :logic
                           (if (consp branches)
                               branches
                             (list (branch-fix :irrelevant)))
                           :exec branches)))
        (cons :if (list branches else))))))