Moved tactic tests from cur-lib to cur-test

cur-lib/cur/stdlib/tactics/standard.rkt

@@ -98,31 +98,3 @@
 ;; Open interactive REPL for tactic DSL; exit with QED command, which
 ;; returns a QED script
 ;(define-syntax interactive-proof)
-
-(module+ test
-  (require
-    rackunit
-    "../bool.rkt")
-  (define-theorem meow (forall (x : Bool) Bool))
-  (proof
-    (intro x)
-    (by-assumption))
-  (define-theorem meow1 (forall (x : Bool) Bool))
-  (proof
-    (obvious)
-    ;; TODO: Add ability to check output
-    #;(print))
-  (define-theorem meow2 (forall (x : Bool) Bool))
-  (proof
-    (intro x)
-    (restart)
-    (intro x)
-    (by-assumption))
-  (define-theorem meow3 (forall (x : Bool) Bool))
-  (proof (obvious))
-  ;; TODO: Fix this unit test so it doesn't require interaction
-  (define-theorem meow4 (forall (x : Bool) Bool))
-  #;(proof (interactive))
-  ;; TODO: Add check-cur-equal? for unit testing?
-  #;(check-pred (curry cur-equal? '(lambda (x : bool) x)))
-  )

cur-test/cur/tests/stdlib/tactics.rkt

@@ -0,0 +1,36 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/tactics/base
+ cur/stdlib/tactics/standard)
+(define-theorem meow (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+   (intro x)
+   (by-assumption)) true)
+ true)
+(define-theorem meow1 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+   (obvious)
+   ;; TODO: Add ability to check output
+   #;(print)) true)
+ true)
+(define-theorem meow2 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+  (intro x)
+  (restart)
+  (intro x)
+  (by-assumption)) true)
+ true)
+(define-theorem meow3 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof (obvious)) true)
+ true)
+;; TODO: Fix this unit test so it doesn't require interaction
+(define-theorem meow4 (forall (x : Bool) Bool))
+#;(proof (interactive))