		Search-engine friendly clone of the ACL2 documentation.

Cgraph-outedges

Make-cgraph-outedges

Basic constructor macro for cgraph-outedges structures.

Syntax

(make-cgraph-outedges [:formulas <formulas>] 
                      [:equivs <equivs>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-cgraph-outedges

(defmacro make-cgraph-outedges (&rest args)
  (std::make-aggregate 'cgraph-outedges
                       args '((:formulas) (:equivs))
                       'make-cgraph-outedges
                       nil))

Function: cgraph-outedges

(defun cgraph-outedges (formulas equivs)
  (declare (xargs :guard (and (cgraph-formulalist-p formulas)
                              (cgraph-equivlist-p equivs))))
  (declare (xargs :guard t))
  (let ((__function__ 'cgraph-outedges))
    (declare (ignorable __function__))
    (b* ((formulas (mbe :logic (cgraph-formulalist-fix formulas)
                        :exec formulas))
         (equivs (mbe :logic (cgraph-equivlist-fix equivs)
                      :exec equivs)))
      (list (cons 'formulas formulas)
            (cons 'equivs equivs)))))