blob: 3d4660b48717cce67e17ea235699ee2338298497 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Set Primitive Projections.
Set Implicit Arguments.
Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
Definition eta_sigma {A} {P : A -> Type} (u : sigT P)
: existT _ (projT1 u) (projT2 u) = u
:= match u with existT _ x y => eq_refl end. (* Toplevel input, characters 0-139:
Error: Pattern-matching expression on an object of inductive type sigT
has invalid information. *)
Definition sum_of_sigT A B (x : sigT (fun b : bool => if b then A else B))
: A + B
:= match x with
| existT _ true a => inl a
| existT _ false b => inr b
end. (* Toplevel input, characters 0-182:
Error: Pattern-matching expression on an object of inductive type sigT
has invalid information. *)
|
