Included Books
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
hons-equal!function
(defun hons-equal! (x y) (declare (xargs :guard t)) (equal x y))
hons-equal!-elimfunction
(defun hons-equal!-elim (x) (cond ((and (nvariablep x) (eq (ffn-symb x) 'hons-equal!)) (cond ((hons-equal (hons-copy (fargn x 1)) (hons-copy (fargn x 2))) *t*) (t (list 'hide x)))) (t x)))
other
(defevaluator evl evl-list ((equal x y) (hons-equal x y) (hons-equal! x y) (hide x)))
hons-equal!-elim-correcttheorem
(defthm hons-equal!-elim-correct (equal (evl x a) (evl (hons-equal!-elim x) a)) :hints (("Goal" :in-theory (enable hons-equal!) :expand ((:free (x) (hide x))))) :rule-classes ((:meta :trigger-fns (hons-equal!))))
in-theory
(in-theory (disable hons-equal! (:e hons-equal!)))