blob: bd53389b4fcfd9404ab817ac8a2f1a8e87389eaa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
Set Primitive Projections.
Set Implicit Arguments.
Set Record Elimination Schemes.
Record prod A B := pair { fst : A ; snd : B }.
Definition f : Set -> Type := fun x => x.
Goal (fst (pair (fun x => x + 1) nat) 0) = 0.
compute.
Undo.
cbv.
Undo.
Opaque fst.
cbn.
Transparent fst.
cbn.
Undo.
simpl.
Undo.
Abort.
Goal f (fst (pair nat nat)) = nat.
compute.
match goal with
| [ |- fst ?x = nat ] => fail 1 "compute failed"
| [ |- nat = nat ] => idtac
end.
reflexivity.
Defined.
Goal fst (pair nat nat) = nat.
unfold fst.
match goal with
| [ |- fst ?x = nat ] => fail 1 "compute failed"
| [ |- nat = nat ] => idtac
end.
reflexivity.
Defined.
Lemma eta A B : forall x : prod A B, x = pair (fst x) (snd x). reflexivity. Qed.
Goal forall x : prod nat nat, fst x = 0.
intros. unfold fst.
Fail match goal with
| [ |- fst ?x = 0 ] => idtac
end.
Abort.
|
