wip35

1 files changed, 10 insertions, 12 deletions

diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
index b892f7f..338843b 100644
--- a/vikalpa/the-little-prover.scm
+++ b/vikalpa/the-little-prover.scm
@@ -17,24 +17,22 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa the-little-prover)
-  #:export (atom? the-little-prover)
+  #:export (the-little-prover)
   #:use-module (vikalpa))
 
-(define (atom? x)
-  (not (pair? x)))
-
 (define (size x)
-  (if (atom? x)
-      0
+  (if (pair? x)
       (+ (size (car x))
-         (size (cdr x)))))
+         (size (cdr x)))
+      0))
 
 (define-system the-little-prover ()
-  (define-primitive-function atom? (x))
-  (define-primitive-function size (x))
-  (define-primitive-function + (x y))
-  (define-primitive-function natural? (x))
-  (define-primitive-function < (x y))
+  (define-function atom? (x)
+    (not (pair? x)))
+  (define-builtin-function size (x))
+  (define-builtin-function + (x y))
+  (define-builtin-function natural? (x))
+  (define-builtin-function < (x y))
   (define-totality-claim natural? natural? <)
   
   ;; Axioms of Equal