		Search-engine friendly clone of the ACL2 documentation.

Smt-computed-hints

Smt-delayed-hint

SMT::SMT-delayed-hints applies the hints kwd-alist and install the smt-computed-hint back.

Signature
(smt-delayed-hint cl kwd-alist) → *

Definitions and Theorems

Function: smt-delayed-hint

(defun smt-delayed-hint (cl kwd-alist)
  (declare (ignore cl))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'smt-delayed-hint))
    (declare (ignorable acl2::__function__))
    (cons ':computed-hint-replacement
          (cons '((smt-computed-hint clause))
                kwd-alist))))