blob: ea122e521f3855a5f74c7004467fb8ea00ff1497 (
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 Nonrecursive Elimination Schemes.
Record notprim : Prop :=
{ irrel : True; relevant : nat }.
|