summaryrefslogtreecommitdiff
path: root/vikalpa/prelude.scm
diff options
context:
space:
mode:
Diffstat (limited to 'vikalpa/prelude.scm')
-rw-r--r--vikalpa/prelude.scm53
1 files changed, 27 insertions, 26 deletions
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))))
+