wip81develop-202001

3 files changed, 16 insertions, 36 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?)
diff --git a/guix.scm b/guix.scm
index 694101d..21460c6 100644
--- a/guix.scm
+++ b/guix.scm
@@ -1,5 +1,5 @@
 ;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+;;; Copyright © 2020, 2021 Masaya Tojo <masaya@tojo.tokyo>
 ;;;
 ;;; This file is part of Vikalpa.
 ;;;
@@ -29,7 +29,7 @@
 (define guile-vikalpa
   (package
     (name "guile-vikalpa")
-    (version "0.0.0")
+    (version "0.1.0")
     (source (string-append (getcwd) "/vikalpa-" version ".tar.gz"))
     (build-system gnu-build-system)
     (native-inputs
diff --git a/vikalpa.scm b/vikalpa.scm
index 3d5e3e5..8dedfb9 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -1553,17 +1553,13 @@
         (get-variables d)
         (get-expression d)))
 
-(define* (system-apropos sys
-                         str
-                         #:key all?)
+(define* (system-apropos sys str)
   (filter-map (lambda (d)
                 (let ((name (format #f "~a" (get-name d))))
-                  (if (and (or all?
-                               (not (string-match "^%" name)))
-                           (string-match (string-append ".*"
-                                                        (regexp-quote str)
-                                                        ".*")
-                                         name))
+                  (if (string-match (string-append ".*"
+                                                   (regexp-quote str)
+                                                   ".*")
+                                    name)
                       (list (get-name d) (show d))
                       #f)))
               (get-definitions sys)))