		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-sort-edges

Signature
(vl-edgesynth-sort-edges priority-clks edgetable) → edgelist
Arguments: priority-clks — Guard (string-listp priority-clks).; edgetable — Guard (vl-edgetable-p edgetable).
Returns: edgelist — Type (vl-edgesynth-edgelist-p edgelist), given the guard.

Definitions and Theorems

Function: vl-edgesynth-sort-edges

(defun vl-edgesynth-sort-edges (priority-clks edgetable)
 (declare (xargs :guard (and (string-listp priority-clks)
                             (vl-edgetable-p edgetable))))
 (declare
  (xargs
       :guard (subsetp-equal priority-clks (alist-keys edgetable))))
 (let ((__function__ 'vl-edgesynth-sort-edges))
   (declare (ignorable __function__))
   (if (atom priority-clks)
       nil
     (cons (cdr (hons-assoc-equal (car priority-clks)
                                  edgetable))
           (vl-edgesynth-sort-edges (cdr priority-clks)
                                    edgetable)))))

Theorem: vl-edgesynth-edgelist-p-of-vl-edgesynth-sort-edges

(defthm vl-edgesynth-edgelist-p-of-vl-edgesynth-sort-edges
 (implies
  (and (force (string-listp priority-clks))
       (force (vl-edgetable-p edgetable))
       (force (subsetp-equal priority-clks (alist-keys edgetable))))
  (b* ((edgelist (vl-edgesynth-sort-edges priority-clks edgetable)))
    (vl-edgesynth-edgelist-p edgelist)))
 :rule-classes :rewrite)

Theorem: len-of-vl-edgesynth-sort-edges

(defthm len-of-vl-edgesynth-sort-edges
  (equal (len (vl-edgesynth-sort-edges priority-clks edgetable))
         (len priority-clks)))

Theorem: consp-of-vl-edgesynth-sort-edges

(defthm consp-of-vl-edgesynth-sort-edges
  (equal (consp (vl-edgesynth-sort-edges priority-clks edgetable))
         (consp priority-clks)))

Theorem: vl-edgesynth-sort-edges-under-iff

(defthm vl-edgesynth-sort-edges-under-iff
  (iff (vl-edgesynth-sort-edges priority-clks edgetable)
       (consp priority-clks)))