acl2 - 如何关闭快速和肮脏的包含替换步骤

Question

当我打断已经出去吃午饭的证明时，我quick-and-dirty-subsumption-replacement-step在回溯中看到了。如何禁用该启发式？

Answer 1

承认以下两种形式后再次尝试证明：

(defun quick-and-dirty-srs-off (cl1 ac)
  (declare (ignore cl1 ac)
           (xargs :mode :logic :guard t))
  nil)

(defattach quick-and-dirty-srs quick-and-dirty-srs-off)