		Search-engine friendly clone of the ACL2 documentation.

Cgraph-edge

Make-cgraph-edge

Basic constructor macro for cgraph-edge structures.

Syntax

(make-cgraph-edge [:match-vars <match-vars>] 
                  [:rule <rule>] 
                  [:subst <subst>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-cgraph-edge

(defmacro make-cgraph-edge (&rest args)
  (std::make-aggregate 'cgraph-edge
                       args '((:match-vars) (:rule) (:subst))
                       'make-cgraph-edge
                       nil))

Function: cgraph-edge

(defun cgraph-edge (match-vars rule subst)
  (declare (xargs :guard (and (pseudo-var-list-p match-vars)
                              (ctrex-rule-p rule)
                              (fgl-object-bindings-p subst))))
  (declare (xargs :guard t))
  (let ((__function__ 'cgraph-edge))
    (declare (ignorable __function__))
    (b* ((match-vars (mbe :logic (pseudo-var-list-fix match-vars)
                          :exec match-vars))
         (rule (mbe :logic (ctrex-rule-fix rule)
                    :exec rule))
         (subst (mbe :logic (fgl-object-bindings-fix subst)
                     :exec subst)))
      (std::prod-cons match-vars
                      (std::prod-cons rule subst)))))