From 32ce95f0cb18145f1e5e307b665a3cd1c1750253 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Tue, 5 Jan 2021 07:55:52 +0900 Subject: wip63 --- vikalpa/prelude.scm | 53 +++++++++++++++++++++++++++-------------------------- 1 file changed, 27 insertions(+), 26 deletions(-) (limited to 'vikalpa') diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 176983c..201e93d 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -163,34 +163,35 @@ (define-system prelude (prelude/measure/natural) (define-proof inexact? - (((2) if-nest) - (() if-same))) + ((rewrite (2) if-nest) + (rewrite () if-same))) (define-proof inexact-predicate - (((1) inexact?) - (() if-not) - ((3 1) inexact?) - ((3 1 1) equal-if-false) - ((3) (eval)) - (() if-same))) + ((rewrite (1) inexact?) + (rewrite () if-not) + (rewrite (3 1) inexact?) + (rewrite (3 1 1) equal-if-false) + (eval (3)) + (rewrite () if-same))) (define-proof positive? - (((2 1 1) (eval)) - ((2 1) if-true) - ((2) if-nest) - (() if-same))) + ((eval (2 1 1)) + (rewrite (2 1) if-true) + (rewrite (2) if-nest) + (rewrite () if-same))) (define-proof positive-predicate - (((1) positive?) - ((2 1) positive?) - ((2 1) less-than-predicate) - ((2) (eval)) - (() if-same))) + ((rewrite (1) positive?) + (rewrite (2 1) positive?) + (rewrite (2 1) less-than-predicate) + (eval (2)) + (rewrite () if-same))) (define-proof negative? - (((2 1) if-nest) - ((2 1) (eval)) - ((2) if-true) - (() if-same))) + ((rewrite (2 1) if-nest) + (eval (2 1)) + (rewrite (2) if-true) + (rewrite () if-same))) (define-proof negative-predicate - (((1) negative?) - ((2 1) negative?) - ((2 1) less-than-predicate) - ((2) (eval)) - (() if-same)))) + ((rewrite (1) negative?) + (rewrite (2 1) negative?) + (rewrite (2 1) less-than-predicate) + (eval (2)) + (rewrite () if-same)))) + -- cgit v1.2.3