summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2022-07-18 02:35:07 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2022-07-18 02:35:07 +0900
commita4331bbef99dc67fe30775d677d368a62810d9b4 (patch)
tree1b1983ff62b3655ff05ba89b99357a658cc751f5
parentb22f11af26fe3108dbd9636b3e5c6973ab57e6dd (diff)
lists/shuffle: Solve Double-rewrite warning.HEADmain
-rw-r--r--lists/shuffle.lisp4
1 files changed, 2 insertions, 2 deletions
diff --git a/lists/shuffle.lisp b/lists/shuffle.lisp
index 61d7e08..20787a4 100644
--- a/lists/shuffle.lisp
+++ b/lists/shuffle.lisp
@@ -32,7 +32,7 @@
(implies (and (consp x)
(< i (len x)))
(perm (remove-nth i x)
- (remove1 (nth i x) x)))
+ (remove1 (nth i x) (double-rewrite x))))
:hints (("Goal" :induct (remove-nth i x))
("Subgoal *1/3.8'"
:cases ((consp (cdr x)))))))
@@ -44,4 +44,4 @@
(member (nth i x) x))))
(defthm perm-shuffle
- (perm (mv-nth 0 (shuffle x state)) x))
+ (perm (mv-nth 0 (shuffle x state)) (double-rewrite x)))