From b60a5fa9bfd8570bb5878492db85a9814f71e028 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 7 Aug 2021 01:02:01 +0900
Subject: peano: Change nat's expression.

---
 peano.lisp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'peano.lisp')

diff --git a/peano.lisp b/peano.lisp
index e5894ce..7d042f2 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -5,7 +5,7 @@
   `(atom ,x))
 
 (defmacro succ (x)
-  `(cons nil ,x))
+  `(cons ,x ,x))
 
 (defmacro pred (x)
   `(cdr ,x))
@@ -13,7 +13,7 @@
 (defun nat? (x)
   (if (z? x)
       (null x)
-      (and (equal (car x) nil)
+      (and (equal (car x) (cdr x))
            (nat? (pred x)))))
 
 (defthm zero-is-nat
-- 
cgit v1.2.3