(s4vec-correct-fn args wrld) → *
Function:
(defun s4vec-correct-fn (args wrld) (declare (xargs :guard t)) (let ((__function__ 's4vec-correct-fn)) (declare (ignorable __function__)) (b* ((fn (std::get-define-current-function wrld)) ((std::defguts guts) (cdr (assoc fn (std::get-define-guts-alist wrld)))) ((std::returnspec retval) (car guts.returnspecs)) (4vec-fn (intern$ (subseq (symbol-name fn) 1 nil) "SV"))) (cons 'defret (cons '<fn>-correct (cons (cons 'equal (cons (cons 's4vec->4vec (cons retval.name 'nil)) (cons (cons 4vec-fn (s4vec-correct-formal-evals guts.formals)) 'nil))) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'enable (cons 4vec-fn (cadr (assoc-keyword :enable args)))) 'nil))) 'nil) 'nil))))))))