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
|
(* Systematic study around issue #9086 *)
Local Set Primitive Projections.
Record pair {A B} := mk { _1 : A; _2 : B _1 }.
Module Folded.
Goal (@mk Prop (fun _ => Prop) True True).(_1).
assert_succeeds (progress (cbn iota delta [_1])).
assert_succeeds (progress (cbv iota delta [_1])).
assert_succeeds (progress (lazy iota delta [_1])).
assert_succeeds (progress simpl).
Opaque _1. (* has an impact on "_1" *)
assert_fails (progress cbn).
assert_fails (progress cbv).
assert_fails (progress lazy).
assert_fails (progress simpl).
Abort.
End Folded.
Module Unfolded.
Goal (@mk Prop (fun _ => Prop) True True).(_1).
lazy delta [_1]. (* move to unfolded form *)
assert_succeeds (progress (cbn iota delta [_1])).
assert_succeeds (progress (cbv iota delta [_1])).
assert_succeeds (progress (lazy iota delta [_1])).
assert_succeeds (progress simpl).
Opaque _1. (* no impact on "unfolded _1" *)
assert_succeeds (progress (cbn iota delta [_1])).
assert_succeeds (progress (cbv iota delta [_1])).
assert_succeeds (progress (lazy iota delta [_1])).
assert_succeeds (progress simpl).
Abort.
End Unfolded.
Module Unfold.
Set Printing Unfolded Projection As Match.
Goal (@mk Prop (fun _ => Prop) True True).(_1).
cbv delta [_1]. (* should internally unfold the projection *)
progress lazy iota. (* allowed by the unfolding *)
Abort.
End Unfold.
|
