aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_054.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2014-05-09 10:13:32 -0400
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-10 15:39:39 +0200
commitc7284415e4bdd3315c84c7d15d140d3fee000bc5 (patch)
treecc8ded3feba7e1da0dd4f7d17b7e5f974de752c3 /test-suite/bugs/closed/HoTT_coq_054.v
parent3f64bd23a343bcd7be0ef07afa7d9e3249df24ec (diff)
Move opened bugs to bugs/opened
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_054.v')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_054.v94
1 files changed, 0 insertions, 94 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
deleted file mode 100644
index f79fe1c1e..000000000
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ /dev/null
@@ -1,94 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
-Inductive Empty : Prop := .
-
-Inductive paths {A : Type} (a : A) : A -> Type :=
- idpath : paths a a.
-
-Notation "x = y :> A" := (@paths A x y) : type_scope.
-Notation "x = y" := (x = y :>_) : type_scope.
-
-Arguments idpath {A a} , [A] a.
-
-Definition idmap {A : Type} : A -> A := fun x => x.
-
-Definition path_sum {A B : Type} (z z' : A + B)
- (pq : match z, z' with
- | inl z0, inl z'0 => z0 = z'0
- | inr z0, inr z'0 => z0 = z'0
- | _, _ => Empty
- end)
-: z = z'.
- destruct z, z', pq; exact idpath.
-Defined.
-
-Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
- := match p with idpath => idpath end.
-
-Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
- (* Fortunately, this unifies properly *)
- (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
- let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
- ap f (path_sum x y pq) = path_sum (f x) (f y)
- (* Coq appears to require *ALL* of the annotations *)
- ((match x as x return match (x, y) with
- (inl x', inl y') => x' = y'
- | (inr x', inr y') => x' = y'
- | _ => Empty
- end -> match (f x, f y) with
- | (inl x', inl y') => x' = y'
- | (inr x', inr y') => x' = y'
- | _ => Empty end with
- | inl x' => match y as y return match y with
- inl y' => x' = y'
- | _ => Empty
- end -> match f y with
- | inl y' => g x' = y'
- | _ => Empty end with
- | inl y' => ap g
- | inr y' => idmap
- end
- | inr x' => match y as y return match y with
- inr y' => x' = y'
- | _ => Empty
- end -> match f y with
- | inr y' => h x' = y'
- | _ => Empty end with
- | inl y' => idmap
- | inr y' => ap h
- end
- end) pq).
- destruct x; destruct y; destruct pq; reflexivity.
-Qed.
-(* Toplevel input, characters 1367-1374:
-Error:
-In environment
-A : Type
-B : Type
-A' : Type
-B' : Type
-g : A -> A'
-h : B -> B'
-x : A + B
-y : A + B
-pq :
-match x with
-| inl x' => match y with
- | inl y' => x' = y'
- | inr _ => Empty
- end
-| inr x' => match y with
- | inl _ => Empty
- | inr y' => x' = y'
- end
-end
-f :=
-fun z : A + B =>
-match z with
-| inl z' => inl (g z')
-| inr z' => inr (h z')
-end : A + B -> A' + B'
-x' : B
-y0 : A + B
-y' : B
-The term "x' = y'" has type "Type" while it is expected to have type
-"Prop" (Universe inconsistency). *)