blob: e83166aaec20e992e0a2e30d06cf9aa69a2cdb1d (
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 }.
|
