diff options
Diffstat (limited to 'vikalpa/prelude.scm')
| -rw-r--r-- | vikalpa/prelude.scm | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index c7ab89e..c61e459 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -102,11 +102,6 @@ (define-function zero? (x) (equal? 0 x)) - (define-function natural? (x) - (and (integer? x) - (or (zero? x) - (< 0 x)))) - (define-axiom pred/succ (x) (implies (natural? x) (equal? (pred (succ x)) x))) @@ -122,8 +117,6 @@ (equal? (< (pred x) x) #t))) (define-totality-claim natural? natural? <) - - (define-function + (x y) (natural? x) (natural? y) @@ -131,13 +124,6 @@ y (succ (+ (pred x) y)))) - (define-proof zero? - () - ()) - - (define-proof natural? - () - ()) (define-proof + (natural? x) ()) |