		Search-engine friendly clone of the ACL2 documentation.

Svtv-overrideline

Make-svtv-overrideline

Basic constructor macro for svtv-overrideline structures.

Syntax

(make-svtv-overrideline [:lhs <lhs>] 
                        [:test <test>] 
                        [:val <val>] 
                        [:entries <entries>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-overrideline

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

Function: svtv-overrideline

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