blob: a6ff78d1270002d095e04847d8721f8e627442d9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Set Implicit Arguments.
Require Import Logic.
Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.
Local Set Nonrecursive Elimination Schemes.
Local Set Primitive Projections.
Record prod (A B : Type) : Type :=
pair { fst : A; snd : B }.
Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x).
|
