diff options
Diffstat (limited to 'vikalpa.scm')
| -rw-r--r-- | vikalpa.scm | 21 |
1 files 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 |