expander-tests

(encapsulate nil
  (local (progn (defun f1 (x) (declare (ignore x)) t)
      (defun f2 (x) (declare (ignore x)) t)
      (defthm f1->f2 (implies (force (f1 x)) (equal (f2 x) t)))
      (defthm f1-true (f1 x))
      (in-theory (disable f1 (:t f1) f2 (:t f2) f1-true (:e tau-system)))
      (make-event (er-let* ((val (defthm? foo
               (equal (cons (f2 x) x) ?)
               :hints (("[1]Goal" :in-theory (enable f1-true))))))
          (cond (val (value '(value-triple t)))
            (t (er soft 'expander-tests "Test failed!")))))
      (make-event (mv-let (erp val state)
          (tool2-fn '(cons (f2 x) x)
            nil
            nil
            state
            '(("[1]Goal" :in-theory (enable f1-true)))
            t
            :all nil
            nil
            t
            'top)
          (cond ((and (eq erp nil)
               (equal val
                 '(((:rewrite f1-true) (:rewrite f1->f2)
                    (:executable-counterpart force)) (cons 't x)))) (value '(value-triple t)))
            (t (er soft 'top "Test failed!"))))))))