diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-20 22:04:09 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-20 22:04:09 +0900 |
| commit | 4f019b8336376f7e39eedbc4ec4645ea547f505b (patch) | |
| tree | 2228aadc46f7c951895d5e2b1f35f3a054cb1b2f | |
| parent | d75c913a514c3a4299502a93d3025b03d2320109 (diff) | |
wip28
| -rw-r--r-- | vikalpa/prelude.scm | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 264773d..8816131 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -119,7 +119,7 @@ (define-axiom </sub1 (x) (implies (natural? x) (equal? (< (sub1 x) x) '#t))) - (define-axiom common-add1 (x y) + (define-theorem common-add1 (x y) (implies (natural? x) (natural? y) (equal? (equal? (add1 x) (add1 y)) |