blob: 77e31e108f2955983d7d99b5c7cd2ccb0320e08d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Set Primitive Projections.
Polymorphic Record pair {A B : Type} : Type :=
prod { pr1 : A; pr2 : B }.
Notation " ( x ; y ) " := (@prod _ _ x y).
Notation " x .1 " := (pr1 x) (at level 3).
Notation " x .2 " := (pr2 x) (at level 3).
Goal ((0; 1); 2).1.2 = 1.
Proof.
cbv.
match goal with
| |- ?t = ?t => exact (eq_refl t)
end.
Qed.
|
