Given an output name and an SVTV, finds the width of that output.
Function:
(defun svtv->out-width (name svtv) (declare (xargs :guard (svtv-p svtv))) (let ((__function__ 'svtv->out-width)) (declare (ignorable __function__)) (b* ((look (hons-assoc-equal name (svtv->outmasks svtv))) ((unless look) (raise "Unknown output: ~x0~%" name) 0)) (integer-length (nfix (cdr look))))))
Theorem:
(defthm natp-of-svtv->out-width (b* ((width (svtv->out-width name svtv))) (natp width)) :rule-classes :type-prescription)
Theorem:
(defthm svtv->out-width-of-svtv-fix-svtv (equal (svtv->out-width name (svtv-fix svtv)) (svtv->out-width name svtv)))
Theorem:
(defthm svtv->out-width-svtv-equiv-congruence-on-svtv (implies (svtv-equiv svtv svtv-equiv) (equal (svtv->out-width name svtv) (svtv->out-width name svtv-equiv))) :rule-classes :congruence)