diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-07 01:02:01 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-07 01:02:01 +0900 |
commit | b60a5fa9bfd8570bb5878492db85a9814f71e028 (patch) | |
tree | a58ebab4c76c8d44938adcc96457cb5262169ae3 | |
parent | 12132a24ad279fd3c1443cb79d52f897acaa49a7 (diff) |
peano: Change nat's expression.
-rw-r--r-- | peano.lisp | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 |