summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-18 02:13:05 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-18 02:13:05 +0900
commite062d5b7a35866b4043c2b325989e1d5a55b46c3 (patch)
treee4f621ff7ef1ca321ef08a2d3d3e7ec115f8f291
parenta03cb62c324489dc4c41f84bace7e53e1d6b0efb (diff)
lists/perm: Solve Free warnings.
-rw-r--r--lists/perm.lisp6
1 files changed, 4 insertions, 2 deletions
diff --git a/lists/perm.lisp b/lists/perm.lisp
index 36253ec..a5b5487 100644
--- a/lists/perm.lisp
+++ b/lists/perm.lisp
@@ -58,11 +58,13 @@
(implies (and (member e x)
(not (member e y)))
(not (perm x y)))
- :hints (("Subgoal *1/3" :cases ((equal (car x) e))))))
+ :hints (("Subgoal *1/3" :cases ((equal (car x) e))))
+ :rule-classes ((:rewrite :match-free :all))))
(defthm perm-transitive
(implies (and (perm x y)
(perm y z))
- (perm x z)))))
+ (perm x z))
+ :rule-classes ((:rewrite :match-free :all)))))
(defequiv perm)