(vl-paramdecl-final-value decl ss) → val
Function:
(defun vl-paramdecl-final-value (decl ss) (declare (xargs :guard (and (vl-paramdecl-p decl) (vl-scopestack-p ss)))) (let ((__function__ 'vl-paramdecl-final-value)) (declare (ignorable __function__)) (b* (((vl-paramdecl decl)) (default (vl-paramtype->default decl.type)) ((unless default) nil) (ctx *vl-fake-context*) ((mv okp ?warnings new-value) (vl-override-parameter-value decl default ss nil ctx))) (and okp new-value))))
Theorem:
(defthm vl-maybe-paramvalue-p-of-vl-paramdecl-final-value (b* ((val (vl-paramdecl-final-value decl ss))) (vl-maybe-paramvalue-p val)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecl-final-value-of-vl-paramdecl-fix-decl (equal (vl-paramdecl-final-value (vl-paramdecl-fix decl) ss) (vl-paramdecl-final-value decl ss)))
Theorem:
(defthm vl-paramdecl-final-value-vl-paramdecl-equiv-congruence-on-decl (implies (vl-paramdecl-equiv decl decl-equiv) (equal (vl-paramdecl-final-value decl ss) (vl-paramdecl-final-value decl-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-paramdecl-final-value-of-vl-scopestack-fix-ss (equal (vl-paramdecl-final-value decl (vl-scopestack-fix ss)) (vl-paramdecl-final-value decl ss)))
Theorem:
(defthm vl-paramdecl-final-value-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-paramdecl-final-value decl ss) (vl-paramdecl-final-value decl ss-equiv))) :rule-classes :congruence)