		Search-engine friendly clone of the ACL2 documentation.

Svtv-outputline

Make-svtv-outputline

Basic constructor macro for svtv-outputline structures.

Syntax

(make-svtv-outputline [:lhs <lhs>] 
                      [:entries <entries>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-outputline

(defmacro make-svtv-outputline (&rest args)
  (std::make-aggregate 'svtv-outputline
                       args '((:lhs) (:entries))
                       'make-svtv-outputline
                       nil))

Function: svtv-outputline

(defun svtv-outputline (lhs entries)
  (declare (xargs :guard (and (lhs-p lhs)
                              (svtv-outentrylist-p entries))))
  (declare (xargs :guard t))
  (let ((__function__ 'svtv-outputline))
    (declare (ignorable __function__))
    (b* ((lhs (mbe :logic (lhs-fix lhs) :exec lhs))
         (entries (mbe :logic (svtv-outentrylist-fix entries)
                       :exec entries)))
      (std::prod-cons lhs entries))))