blob: c981207e6bfb91f6defafd5052941fc3cf79dd1b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Set Primitive Projections.
Record foo (A : Type) :=
{ bar : Type ; baz := Set; bad : baz = bar }.
Set Record Elimination Schemes.
Record notprim : Prop :=
{ irrel : True; relevant : nat }.
|