(vl-edgesynth-edge->expr x) → expr
Function:
(defun vl-edgesynth-edge->expr (x) (declare (xargs :guard (vl-edgesynth-edge-p x))) (let ((__function__ 'vl-edgesynth-edge->expr)) (declare (ignorable __function__)) (vl-evatom->expr x)))
Theorem:
(defthm return-type-of-vl-edgesynth-edge->expr (implies (and (vl-edgesynth-edge-p x)) (b* ((expr (vl-edgesynth-edge->expr x))) (and (vl-expr-p expr) (vl-idexpr-p expr) (vl-expr->finaltype expr) (equal (vl-expr->finalwidth expr) 1)))) :rule-classes :rewrite)