disabled test that cause setup errors

This commit is contained in:
William J. Bowman 2015-09-25 20:10:32 -04:00
parent e54c7e5bb5
commit 8aabbc219b
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
3 changed files with 6 additions and 1 deletions

View File

@ -8,7 +8,8 @@
(module+ test (module+ test
(require rackunit "bool.rkt") (require rackunit "bool.rkt")
(check-equal? ;; Disabled until #22 fixed
#;(check-equal?
(case* Maybe Type (some Bool true) (Bool) (case* Maybe Type (some Bool true) (Bool)
(lambda* (A : Type) (x : (Maybe A)) A) (lambda* (A : Type) (x : (Maybe A)) A)
[(none (A : Type)) IH: () [(none (A : Type)) IH: ()

View File

@ -47,6 +47,7 @@
(check-equal? (nat-equal? z (s z)) false) (check-equal? (nat-equal? z (s z)) false)
(check-equal? (nat-equal? (s z) (s z)) true)) (check-equal? (nat-equal? (s z) (s z)) true))
#| TODO: Disabled until #20 fixed
(define (even? (n : Nat)) (define (even? (n : Nat))
(elim Nat Type (lambda (x : Nat) Bool) (elim Nat Type (lambda (x : Nat) Bool)
false false
@ -80,3 +81,4 @@
(check-equal? (check-equal?
(odd? (s (s (s z)))) (odd? (s (s (s z))))
true)) true))
|#

View File

@ -62,6 +62,7 @@
(qed thm:proj2 proof:proj2) (qed thm:proj2 proof:proj2)
#| TODO: Disabled until #22 fixed
(data Or : (forall* (A : Type) (B : Type) Type) (data Or : (forall* (A : Type) (B : Type) Type)
(left : (forall* (A : Type) (B : Type) (a : A) (Or A B))) (left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
(right : (forall* (A : Type) (B : Type) (b : B) (Or A B)))) (right : (forall* (A : Type) (B : Type) (b : B) (Or A B))))
@ -79,6 +80,7 @@
A A c))) A A c)))
(qed thm:A-or-A proof:A-or-A) (qed thm:A-or-A proof:A-or-A)
|#
(data == : (forall* (A : Type) (x : A) (-> A Type)) (data == : (forall* (A : Type) (x : A) (-> A Type))
(refl : (forall* (A : Type) (x : A) (== A x x)))) (refl : (forall* (A : Type) (x : A) (== A x x))))