suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Added Or, but can't seem to use it

Browse Source
This commit is contained in:
William J. Bowman 2015-09-25 19:32:18 -04:00
parent 4c9c6b4e60
commit f05be17fdf
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
stdlib/prop.rkt
View File

@ -62,5 +62,23 @@
(qed thm:proj2 proof:proj2)
(data Or : (forall* (A : Type) (B : Type) Type)
(left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
(right : (forall* (A : Type) (B : Type) (b : B) (Or A B))))
(define-theorem thm:A-or-A
(forall* (A : Type) (o : (Or A A)) A))
(define proof:A-or-A
(lambda* (A : Type) (c : (Or A A))
;; TODO: What should the motive be?
(elim Or Type (lambda* (A : Type) (B : Type) (c : (Or A B)) A)
(lambda* (A : Type) (B : Type) (a : A) a)
;; TODO: How do we know B is A?
(lambda* (A : Type) (B : Type) (b : B) b)
A A c)))
(qed thm:A-or-A proof:A-or-A)
(data == : (forall* (A : Type) (x : A) (-> A Type))
(refl : (forall* (A : Type) (x : A) (== A x x))))