(vl-bindcontext->shortdescription x) → *
Function:
(defun vl-bindcontext->shortdescription (x) (declare (xargs :guard (vl-bindcontext-p x))) (let ((__function__ 'vl-bindcontext->shortdescription)) (declare (ignorable __function__)) (b* ((x (vl-bindcontext-fix x))) (case (tag x) (:vl-interface (cat "interface " (vl-interface->name x))) (:vl-module (cat "module " (vl-module->name x))) (:vl-design "design (top level)") (otherwise (progn$ (impossible) ""))))))
Theorem:
(defthm vl-bindcontext->shortdescription-of-vl-bindcontext-fix-x (equal (vl-bindcontext->shortdescription (vl-bindcontext-fix x)) (vl-bindcontext->shortdescription x)))
Theorem:
(defthm vl-bindcontext->shortdescription-vl-bindcontext-equiv-congruence-on-x (implies (vl-bindcontext-equiv x x-equiv) (equal (vl-bindcontext->shortdescription x) (vl-bindcontext->shortdescription x-equiv))) :rule-classes :congruence)