From 781074d9360e125913d12b88dada5f100752cb77 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 29 Nov 2020 04:33:21 +0900
Subject: wip40

---
 vikalpa/prelude.scm | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 83f3b6a..5b70a72 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -57,7 +57,7 @@
   (define-function natural? (x)
     (and (integer? x)
          (or (zero? x)
-             (< x 0))))
+             (< 0 x))))
 
   (define-totality-claim natural? natural? <)
 
@@ -123,10 +123,19 @@
              (equal? (< (pred x) x) #t)))
 
   (define-function + (x y)
-    (if (zero? 0 x)
-        y
-        (succ (+ (pred x) y))))
+    (if (natural? x)
+        (if (zero? x)
+            y
+            (succ (+ (pred x) y)))
+        'undeifned<+>))
 
+  (define-proof +
+    (natural? x)
+    (((2) if-nest)
+     ((2 3) less/pred)
+     ((2) if-same)
+     (() if-same)))
+  
   ;; (define-proof if-implies
   ;;   ()
   ;;   (((1) if-same (set x x))
-- 
cgit v1.2.3