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

【问题标题】：How do I turn off quick-and-dirty-subsumption-replacement-step如何关闭快速和肮脏的包含替换步骤
【发布时间】：2016-04-20 10:38:32
【问题描述】：

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

【问题讨论】：

标签： acl2

【解决方案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)

【讨论】：