From 60a1d48a4afdb139caa9936895b3f1833d6a7926 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Wed, 25 Nov 2020 09:29:38 +0900 Subject: wip35 --- vikalpa/the-little-prover.scm | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) (limited to 'vikalpa/the-little-prover.scm') 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 . (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 -- cgit v1.2.3