1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
Set Universe Polymorphism.
Set Primitive Projections.
Set Implicit Arguments.
Record sigT {A : Type} (P : A -> Type) := existT { projT1 : A; projT2 : P projT1 }.
Arguments existT {A} _ _ _.
Definition unpack_sigma' {A} {P : A -> Type} (Q : sigT P -> Type) (u : sigT P) :
Q (existT _ (projT1 u) (projT2 u)) -> Q u
:=
fun H =>
(let (x,p) as u return (Q (existT _ (projT1 u) (projT2 u)) -> Q u) := u in fun x : Q (existT _ _ p) => x) H. (* success *)
Definition unpack_sigma {A} {P : A -> Type} (Q : sigT P -> Type) (u : sigT P) :
Q (existT _ (projT1 u) (projT2 u)) -> Q u
:=
fun H =>
(let (x,p) as u return (Q (existT _ (projT1 u) (projT2 u)) -> Q u) := u in fun x => x) H.
(* Toplevel input, characters 219-229:
Error:
In environment
A : Type
P : A -> Type
Q : sigT P -> Type
u : sigT P
H : Q {| projT1 := projT1 u; projT2 := projT2 u |}
x : A
p : P x
The term
"fun
x : Q
{|
projT1 := projT1 {| projT1 := x; projT2 := p |};
projT2 := projT2 {| projT1 := x; projT2 := p |} |} => x" has type
"Q
{|
projT1 := projT1 {| projT1 := x; projT2 := p |};
projT2 := projT2 {| projT1 := x; projT2 := p |} |} ->
... "
*)
|
