blob: 436a00585bc300b1a36bbb507173acbfee5721a4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Set Primitive Projections.
Record foo := mkFoo { proj1 : bool; proj2 : bool }.
Definition x := mkFoo true false.
Definition proj x := proj2 x.
Lemma oops : proj = fun x => proj1 x.
Proof. Fail native_compute; reflexivity. Abort.
(*
Lemma bad : False.
assert (proj1 x = proj x).
rewrite oops; reflexivity.
discriminate.
Qed.
Print Assumptions bad.
*)
|
