From 6ac3c8c7d47cb68d0edc87dbf9a3d3dc1610bbd4 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 21 Nov 2020 05:00:09 +0900
Subject: wip30

---
 vikalpa.scm | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index cc88c06..f4ef953 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -27,6 +27,7 @@
             system-macros
             system-theorems
             system-axioms
+            system-totality-claims
             define-system
             define-axiom
             define-theorem
@@ -35,9 +36,8 @@
             define-proof
             define-totality-claim
             define-syntax-rules
-            total/natural?
-            induction
-            size add1 sub1 natural?)
+            succ
+            pred)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
@@ -335,7 +335,7 @@
 (define (system-proofs sys)
   (list-ref sys 2))
 
-(define (system-totality-claims sys)
+(define/guard (system-totality-claims (sys system?))
   (list-ref sys 3))
 
 (define (totality-claim id nat? less-than)
@@ -621,10 +621,16 @@
           (expand-let (cdr x))))
    (else x)))
 
+(define (succ x)
+  (+ x 1))
+
+(define (pred x)
+  (- x 1))
+
 (define (natural->expr n)
   (if (zero? n)
       ''0
-      `(add1 ,(natural->expr (sub1 n)))))
+      `(succ ,(natural->expr (pred n)))))
 
 (define (pair->expr x)
   (if (pair? x)
@@ -1051,6 +1057,11 @@
   (parameterize ([current-system parent])
     (define-primitive-function not (x))
     (define-primitive-function equal? (x y))
+    (define-primitive-function cons (x y))
+    (define-primitive-function car (x))
+    (define-primitive-function cdr (x))
+    (define-primitive-function succ (x))
+    (define-primitive-function pred (x))
     (current-system)))
 
 (define-syntax define-system
-- 
cgit v1.2.3