diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-08 08:04:26 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-08 08:04:26 +0900 |
| commit | 3a97b30ca886095bb204f25271f0b256f670f697 (patch) | |
| tree | acdf047344efe9535ca54d7b500dd2adaf0ae2c3 | |
| parent | 4d4bfc8ab6133c41d8b7ff3c281de0f4ef61e5b3 (diff) | |
wip7
| -rw-r--r-- | rabbit-prover.scm | 34 |
1 files changed, 15 insertions, 19 deletions
diff --git a/rabbit-prover.scm b/rabbit-prover.scm index fde842d..a3f0a58 100644 --- a/rabbit-prover.scm +++ b/rabbit-prover.scm @@ -619,43 +619,40 @@ (define current-book (make-parameter '())) -(define (add-book b x) - (cond ((assoc (proposition-name x) b) - => (lambda (prop) - (if (equal? x prop) - b - (error "add-book: error")))) - (else (cons x b)))) +(define (add-book x) + (let ((b (current-book))) + (current-book + (cond ((assoc (proposition-name x) b) + => (lambda (prop) + (if (equal? x prop) + b + (error "add-book: error")))) + (else (cons x b)))))) (define-syntax define-axiom (syntax-rules () ((_ name (var ...) expr) (current-book - (add-book (current-book) - (axiom 'name '(var ...) 'expr)))))) + (add-book (axiom 'name '(var ...) 'expr)))))) (define-syntax define-theorem (syntax-rules () ((_ name (var ...) expr) - (current-book - (add-book (current-book) - (theorem 'name '(var ...) 'expr)))))) + (add-book (theorem 'name '(var ...) 'expr))))) (define-syntax define-function (syntax-rules () ((_ name (var ...) expr) (let ((f (function 'name '(var ...) 'expr))) - (current-book (add-book (current-book) f)) + (add-book f) f)))) (define-syntax define-macro (syntax-rules () ((_ name () ((lhs1 . lhs2) rhs) ...) - (current-book - (add-book (current-book) - (macro 'name - (list (mrule (all-vars 'lhs2) '(lhs1 . lhs2) 'rhs) - ...))))))) + (add-book (macro 'name + (list (mrule (all-vars 'lhs2) '(lhs1 . lhs2) 'rhs) + ...)))))) (define-syntax define-book (syntax-rules () @@ -742,7 +739,6 @@ (equal? (app (app x y) z) (app x (app y z))))) - (define (size x) (if (pair? x) (+ 1 |