diff --git a/cur-lib/cur/stdlib/tactics/standard.rkt b/cur-lib/cur/stdlib/tactics/standard.rkt index d2b83df..0c1831b 100644 --- a/cur-lib/cur/stdlib/tactics/standard.rkt +++ b/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))) - ) diff --git a/cur-test/cur/tests/stdlib/tactics.rkt b/cur-test/cur/tests/stdlib/tactics.rkt new file mode 100644 index 0000000..c33d129 --- /dev/null +++ b/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))