blob: 7754934c0b90644be7f2b434d2d9556e5e4b6a5c (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Set Primitive Projections.
Record unit : Set := tt {}.
Fail Check fun x : unit => eq_refl : tt = x.
Fail Check fun x : unit => eq_refl : x = tt.
Fail Check fun x y : unit => (eq_refl : x = tt) : x = y.
Fail Check fun x y : unit => eq_refl : x = y.
Record ok : Set := tt' { a : unit }.
Record nonprim : Prop := { undef : unit }.
Record prim : Prop := { def : True }.
|
