|
|
|---|
|
|
|
|---|
Recognize a sparse vector in an R1CS constraint.
;; A sparse vector, represented as a list of pairs where each pair contains a ;; coefficient and a pseudo-var. Pseudo-vars not mentioned have an implicit ;; coefficient of 0. (defund sparse-vectorp (vec) (declare (xargs :guard t)) (if (atom vec) (equal vec nil) (let ((item (first vec))) (and (sparse-vector-elementp item) (sparse-vectorp (rest vec))))))