Human-readable description of what kind of module element this is.
(vl-genelement->short-kind-string x) → str
Function:
(defun vl-genelement->short-kind-string (x) (declare (xargs :guard (vl-genelement-p x))) (let ((__function__ 'vl-genelement->short-kind-string)) (declare (ignorable __function__)) (vl-genelement-case x :vl-genbase (vl-modelement->short-kind-string x.item) :vl-genloop "generate loop" :vl-genif "generate if statement" :vl-gencase "generate case statement" :vl-genbegin "generate" :vl-genarray "generate loop")))
Theorem:
(defthm stringp-of-vl-genelement->short-kind-string (b* ((str (vl-genelement->short-kind-string x))) (stringp str)) :rule-classes :type-prescription)