Bind a function's parameter names to their values.
(vl-fundecl-param-sigma x) → sigma
Function:
(defun vl-fundecl-param-sigma (x) (declare (xargs :guard (vl-paramdecllist-p x))) (let ((__function__ 'vl-fundecl-param-sigma)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((vl-paramdecl x1) (vl-paramdecl-fix (car x))) ((unless (and (eq (vl-paramtype-kind x1.type) :vl-implicitvalueparam) (vl-implicitvalueparam->default x1.type))) (raise "Bad parameter for param-sigma: ~x0." x1))) (cons (cons x1.name (vl-implicitvalueparam->default x1.type)) (vl-fundecl-param-sigma (cdr x))))))
Theorem:
(defthm vl-sigma-p-of-vl-fundecl-param-sigma (b* ((sigma (vl-fundecl-param-sigma x))) (vl-sigma-p sigma)) :rule-classes :rewrite)