From f05be17fdf61ab9dcf4fe4f64de5b83118329aca Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 25 Sep 2015 19:32:18 -0400 Subject: [PATCH] Added Or, but can't seem to use it --- stdlib/prop.rkt | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt index c92889d..998eaa2 100644 --- a/stdlib/prop.rkt +++ b/stdlib/prop.rkt @@ -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))))