From a4331bbef99dc67fe30775d677d368a62810d9b4 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Mon, 18 Jul 2022 02:35:07 +0900 Subject: lists/shuffle: Solve Double-rewrite warning. --- lists/shuffle.lisp | 4 ++-- 1 file 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))) -- cgit v1.2.3