From 107ff1ce2460045e30961dd5679c9e20ec1d57a9 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Mon, 30 Nov 2020 14:13:52 +0900 Subject: wip42 --- vikalpa/prelude.scm | 14 -------------- 1 file changed, 14 deletions(-) (limited to 'vikalpa') 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) ()) -- cgit v1.2.3