Trans-hint-option
- Signature
(trans-hint-option opt val state) → *
Definitions and Theorems
Function: trans-hint-option
(defun trans-hint-option (opt val state)
(declare (xargs :stobjs (state)))
(declare (xargs :guard t))
(let ((acl2::__function__ 'trans-hint-option))
(declare (ignorable acl2::__function__))
(cond
((equal opt ':functions)
(trans-functions val state))
((equal opt ':hypotheses)
(trans-hypotheses val state))
((equal opt ':wrld-len)
(er
hard?
'smtlink-process-user-hint->trans-hint-option
"User trying to access internal parameter ~
wrld-len!"))
(t val))))
