Filtering...

use-by-hint

books/clause-processors/use-by-hint

Included Books

remove-hyp bstar
other
(in-package "ACL2")
include-book
(include-book "remove-hyp")
include-book
(include-book "std/util/bstar" :dir :system)
use-by-hintfunction
(defun use-by-hint (x) (declare (ignore x)) t)
in-theory
(in-theory (disable use-by-hint
    (use-by-hint)
    (:type-prescription use-by-hint)))
use-by-computed-hintfunction
(defun use-by-computed-hint
  (clause)
  (declare (xargs :mode :program))
  (case-match clause
    ((('not ('use-by-hint ('quote rule . &) . &) . &) . &) `(:computed-hint-replacement ('(:by ,RULE :do-not '(preprocess simplify)))
        :clause-processor remove-first-hyp-cp))
    (& nil)))
use-these-hintsfunction
(defun use-these-hints (x) (declare (ignore x)) t)
in-theory
(in-theory (disable use-these-hints
    (use-these-hints)
    (:type-prescription use-these-hints)))
use-these-hints-hintfunction
(defun use-these-hints-hint
  (clause)
  (case-match clause
    ((('not ('use-these-hints ('quote the-hints . &) . &) . &) . &) `(:computed-hint-replacement ,THE-HINTS
        :clause-processor remove-first-hyp-cp))
    (& nil)))