(vl-simplenet->nettype x) → nettype
Function:
(defun vl-simplenet->nettype (x) (declare (xargs :guard (vl-vardecl-p x))) (declare (xargs :guard (vl-simplenet-p x))) (let ((__function__ 'vl-simplenet->nettype)) (declare (ignorable __function__)) (b* (((vl-vardecl x) x)) (vl-nettypename-fix x.nettype))))
Theorem:
(defthm vl-nettypename-p-of-vl-simplenet->nettype (b* ((nettype (vl-simplenet->nettype x))) (vl-nettypename-p nettype)) :rule-classes :rewrite)
Theorem:
(defthm vl-simplenet->nettype-of-vl-vardecl-fix-x (equal (vl-simplenet->nettype (vl-vardecl-fix x)) (vl-simplenet->nettype x)))
Theorem:
(defthm vl-simplenet->nettype-vl-vardecl-equiv-congruence-on-x (implies (vl-vardecl-equiv x x-equiv) (equal (vl-simplenet->nettype x) (vl-simplenet->nettype x-equiv))) :rule-classes :congruence)