From 12132a24ad279fd3c1443cb79d52f897acaa49a7 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Fri, 6 Aug 2021 01:21:24 +0900 Subject: peano: associativity-of-nat*: Unuse nat*-commutative. --- peano.lisp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'peano.lisp') diff --git a/peano.lisp b/peano.lisp index 5028a13..e5894ce 100644 --- a/peano.lisp +++ b/peano.lisp @@ -128,7 +128,4 @@ (nat? z)) (equal (nat* x (nat* y z)) (nat* (nat* x y) z))) - :hints (("Goal" :in-theory (disable nat*-commutative) - :use ((:instance nat*-commutative - (x (cdr z)) - (y (nat* x y))))))) + :hints (("Goal" :in-theory (disable nat*-commutative)))) -- cgit v1.2.3