		Search-engine friendly clone of the ACL2 documentation.

3col4vecline

Make-3col4vecline

Basic constructor macro for 3col4vecline structures.

Syntax

(make-3col4vecline [:label <label>] 
                   [:val <val>] 
                   [:val2 <val2>])

This is the usual way to construct 3col4vecline structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-3col4vecline

(defmacro make-3col4vecline (&rest args)
  (std::make-aggregate '3col4vecline
                       args '((:label) (:val) (:val2))
                       'make-3col4vecline
                       nil))

Function: 3col4vecline

(defun 3col4vecline (label val val2)
  (declare (xargs :guard (and (msgp label)
                              (maybe-4vec-p val)
                              (maybe-4vec-p val2))))
  (declare (xargs :guard t))
  (let ((__function__ '3col4vecline))
    (declare (ignorable __function__))
    (b* ((label (mbe :logic (msg-fix label)
                     :exec label))
         (val (mbe :logic (maybe-4vec-fix val)
                   :exec val))
         (val2 (mbe :logic (maybe-4vec-fix val2)
                    :exec val2)))
      (std::prod-cons label (std::prod-cons val val2)))))