diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-08 08:08:41 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-08 08:08:41 +0900 |
| commit | cd7427e42b773bc787a00c12d8f7bff569bd9d85 (patch) | |
| tree | 35c25462c980f3a4df98de5b0b1cd5997e814b99 | |
| parent | 3a97b30ca886095bb204f25271f0b256f670f697 (diff) | |
wip8
| -rw-r--r-- | rabbit-prover.scm | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/rabbit-prover.scm b/rabbit-prover.scm index a3f0a58..b5e7fbc 100644 --- a/rabbit-prover.scm +++ b/rabbit-prover.scm @@ -632,8 +632,7 @@ (define-syntax define-axiom (syntax-rules () ((_ name (var ...) expr) - (current-book - (add-book (axiom 'name '(var ...) 'expr)))))) + (add-book (axiom 'name '(var ...) 'expr))))) (define-syntax define-theorem (syntax-rules () @@ -720,7 +719,7 @@ ((or x . xs) (if x x (or . xs)))) (define-macro atom? () ((atom? x) (not (pair? x)))) - + (define-axiom if-not (x y z) (equal? (if (not x) y |