		Search-engine friendly clone of the ACL2 documentation.

Svtv-line

Make-svtv-line

Basic constructor macro for svtv-line structures.

Syntax

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

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-line

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

Function: svtv-line

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