diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-29 04:33:21 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-29 04:33:21 +0900 |
commit | 781074d9360e125913d12b88dada5f100752cb77 (patch) | |
tree | cb393bde90f7a771599762f833b8dd1ebcdad717 /vikalpa/prelude.scm | |
parent | f6a8c75a6d704367bb6f1a443a326b92a06ff81b (diff) |
wip40
Diffstat (limited to 'vikalpa/prelude.scm')
-rw-r--r-- | vikalpa/prelude.scm | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 83f3b6a..5b70a72 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -57,7 +57,7 @@ (define-function natural? (x) (and (integer? x) (or (zero? x) - (< x 0)))) + (< 0 x)))) (define-totality-claim natural? natural? <) @@ -123,10 +123,19 @@ (equal? (< (pred x) x) #t))) (define-function + (x y) - (if (zero? 0 x) - y - (succ (+ (pred x) y)))) + (if (natural? x) + (if (zero? x) + y + (succ (+ (pred x) y))) + 'undeifned<+>)) + (define-proof + + (natural? x) + (((2) if-nest) + ((2 3) less/pred) + ((2) if-same) + (() if-same))) + ;; (define-proof if-implies ;; () ;; (((1) if-same (set x x)) |