Centaur-specific linter check.
Theorem: vl-design-p-of-vl-centaur-seqcheck-hook
(defthm vl-design-p-of-vl-centaur-seqcheck-hook (vl-design-p (vl-centaur-seqcheck-hook x)))
Function: vl-centaur-seqcheck-hook-default
(defun vl-centaur-seqcheck-hook-default (x) (declare (xargs :guard (vl-design-p x))) (vl-design-fix x))