From bbc57fce02f41e3abdd36669036d0de3983e3ff0 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Tue, 17 Nov 2020 13:18:19 +0900 Subject: wip20 --- vikalpa.scm | 66 +------------------------------------------------------------ 1 file changed, 1 insertion(+), 65 deletions(-) diff --git a/vikalpa.scm b/vikalpa.scm index 335c653..7007be4 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -1216,71 +1216,7 @@ ((3 2 1) if-false) ((3 2) equal-same) ((3) if-same) - (() if-same))) - - #; - (rewrite (app/system) - '(if (natural? (size (app a b))) - (if (atom? a) - '#t - (< (size (app (cdr a) b)) - (size (app a b)))) - '#t) - '(((2 3 2 1) app) - ((2 3 2 1) if-nest) - ((2 3 1 1) cdr/cons (set x (car a))) - ((2 3) if-same (set x (atom? (cons (car a) (app (cdr a) b))))) - ((2 3 3) size/cdr) - ((2 3 1) atom/cons) - ((2 3) if-false) - ((2) if-same) - (() if-same))) - #; - (rewrite (app/system) - '(if (atom? a) - (equal? (app (app a b) c) - (app a (app b c))) - (if (equal? (app (app (cdr a) b) c) - (app (cdr a) (app b c))) - (equal? (app (app a b) c) - (app a (app b c))) - '#t)) - '(((2 2) app) - ((2 2) if-nest-t) - ((2 1 1) app) - ((2 1 1) if-nest-t) - ((2) equal-same) - ((3 2 1 1) app) - ((3 2 1 1) if-nest-f) - ((3 2 2) app) - ((3 2 2) if-nest-f) - ((3 2 2 2) equal-if) - ((3 2 1) app) - ((3 2 1 3 1) car/cons) - ((3 2 1 3 2 1) cdr/cons) - ((3 2 1 1) atom/cons) - ((3 2 1) if-false) - ((3 2) equal-same) - ((3) if-same) - (() if-same))) - ) - -(define-system test/system (prelude) - (define-function id (x) - x) - - (define-function even? (n) - (if (zero? n) - '#t - (if (= n '1) - '#f - (if (even? (- n '2)) - '#t - '#f)))) - - (define-theorem even-n+4 (n) - (equal? (even? n) (even? (+ n '4)))) - ) + (() if-same)))) (define (size x) (if (pair? x) -- cgit v1.2.3