computed-hint-rewrite

(defun computed-hint-rewrite
  (term hyps provep cl hist pspv wrld ctx state)
  (mv-let (rcnst signal)
    (simplify-clause-rcnst cl hist pspv wrld)
    (declare (ignore signal))
    (let* ((ens (access rewrite-constant rcnst :current-enabled-structure)) (gstack nil))
      (mv-let (flg hyps-type-alist ttree)
        (hyps-type-alist hyps ens wrld state)
        (cond (flg (er hard
              ctx
              "~x0 found a contradiction in the hypotheses."
              'computed-hint-rewrite))
          (t (sl-let (new-term new-ttree)
              (rewrite-entry (rewrite term nil 'computed-hint-rewrite)
                :rdepth (rewrite-stack-limit wrld)
                :type-alist hyps-type-alist
                :obj provep
                :geneqv (if (member-eq provep '(t nil))
                  *geneqv-iff*
                  nil)
                :pequiv-info nil
                :fnstack nil
                :ancestors nil
                :backchain-limit (backchain-limit wrld :rewrite)
                :step-limit (initial-step-limit wrld state)
                :simplify-clause-pot-lst nil
                :rcnst rcnst
                :gstack gstack
                :ttree ttree)
              (declare (ignorable step-limit))
              (cons new-term new-ttree))))))))