blob: cbd773d079256e691dd66016758a02c2b5d10689 (
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
48
49
50
51
52
53
|
Module A.
Set Primitive Projections.
Record hSet : Type := BuildhSet { setT : Type; iss : True }.
Ltac head_hnf_under_binders x :=
match eval hnf in x with
| ?f _ => head_hnf_under_binders f
| (fun y => ?f y) => head_hnf_under_binders f
| ?y => y
end.
Goal forall s : hSet, True.
intros.
let x := head_hnf_under_binders setT in pose x.
set (foo := eq_refl (@setT )). generalize foo. simpl. cbn.
Abort.
End A.
Module A'.
Set Universe Polymorphism.
Set Primitive Projections.
Record hSet (A : Type) : Type := BuildhSet { setT : Type; iss : True }.
Ltac head_hnf_under_binders x :=
match eval compute in x with
| ?f _ => head_hnf_under_binders f
| (fun y => ?f y) => head_hnf_under_binders f
| ?y => y
end.
Goal forall s : @hSet nat, True.
intros.
let x := head_hnf_under_binders setT in pose x.
set (foo := eq_refl (@setT nat)). generalize foo. simpl. cbn.
Abort.
End A'.
Set Primitive Projections.
Record hSet : Type := BuildhSet { setT : Type; iss : True }.
Ltac head_hnf_under_binders x :=
match eval hnf in x with
| ?f _ => head_hnf_under_binders f
| (fun y => ?f y) => head_hnf_under_binders f
| ?y => y
end.
Goal setT = setT.
progress unfold setT. (* should not succeed *)
match goal with
| |- (fun h => setT h) = (fun h => setT h) => fail 1 "should not eta-expand"
| _ => idtac
end. (* should not fail *)
Abort.
Goal forall h, setT h = setT h.
Proof. intro. progress unfold setT.
|
