diff options
Diffstat (limited to 'examples/prelude.scm')
| -rw-r--r-- | examples/prelude.scm | 34 |
1 files changed, 9 insertions, 25 deletions
diff --git a/examples/prelude.scm b/examples/prelude.scm index f171b6e..39aa67a 100644 --- a/examples/prelude.scm +++ b/examples/prelude.scm @@ -17,15 +17,9 @@ ;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. (define-module (vikalpa prelude) - #:export (size prelude) + #:export (prelude) #:use-module (vikalpa)) -(define (size x) - (if (pair? x) - (+ (size (car x)) - (size (cdr x))) - 1)) - (define-syntax-rule (define-axiom/is p1 p2) (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x)))) @@ -177,7 +171,6 @@ (define-theorem/is exact-zero? natural?) (define-theorem/is exact-positive-integer? natural?) - (set-measure-predicate natural?) (set-measure-less-than <) @@ -261,7 +254,13 @@ (define-core-function cons (x y) cons) (define-core-function/guard car (x) (pair? x) car) (define-core-function/guard cdr (x) (pair? x) cdr) - (define-core-function size (x) size)) + (define-function size (x) + (if (pair? x) + (+ (size (car x)) + (size (cdr x))) + 1)) + (admit size)) + (define-system prelude (prelude/pair) (define-proof inexact? @@ -369,21 +368,6 @@ (eval (2)) (rewrite () if-same))) - #; - (define-proof (natural? and not exact-zero? implies exact-positive-integer?) - ((rewrite (1) natural?) - (rewrite () if-same (set x (exact-zero? x))) - (rewrite (2 1) if-nest) - (rewrite (2) if-true) - (rewrite (2) if-not) - (rewrite (2) if-nest) - (rewrite (3 1) if-nest) - (rewrite (3 2) if-not) - (rewrite (3 2) if-nest) - (rewrite (3 2) (predicate exact-positive-integer?)) - (rewrite (3) if-same) - (rewrite () if-same))) - (define-proof (+ (-> natural? natural? natural?)) ((induction (2 2) (natural-induction-+ x y)) (rewrite (2 2 2 1) (+ natural? natural?)) @@ -408,7 +392,7 @@ ((rewrite (1) exact-zero?) (rewrite (2 1 1) equal-if) (eval (2)) - (rewrite () if-same))) + (rewrite () if-same))) (define-proof (is exact-positive-integer? natural?) ((rewrite (2 1) natural?) |