blob: 230b4beb6cb2ff61d4ba664f26181182b03d9b21 (
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(*I'd like the final [Check] in the following to work:*)
Ltac fin_eta_expand :=
[ > lazymatch goal with
| [ H : _ |- _ ] => clear H
end..
| lazymatch goal with
| [ H : ?T |- ?T ]
=> exact H
| [ |- ?G ]
=> fail 0 "No hypothesis matching" G
end ];
let n := numgoals in
tryif constr_eq numgoals 0
then idtac
else fin_eta_expand.
Ltac pre_eta_expand x :=
let T := type of x in
let G := match goal with |- ?G => G end in
unify T G;
unshelve econstructor;
destruct x;
fin_eta_expand.
Ltac eta_expand x :=
let v := constr:(ltac:(pre_eta_expand x)) in
idtac v;
let v := (eval cbv beta iota zeta in v) in
exact v.
Notation eta_expand x := (ltac:(eta_expand x)) (only parsing).
Ltac partial_unify eqn :=
lazymatch eqn with
| ?x = ?x => idtac
| ?f ?x = ?g ?y
=> partial_unify (f = g);
(tryif unify x y then
idtac
else tryif has_evar x then
unify x y
else tryif has_evar y then
unify x y
else
idtac)
| ?x = ?y
=> idtac;
(tryif unify x y then
idtac
else tryif has_evar x then
unify x y
else tryif has_evar y then
unify x y
else
idtac)
end.
Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" :=
let old_record' := eta_expand old_record in
partial_unify (old_record = new_record);
eexact new_record.
Set Implicit Arguments.
Record prod A B := pair { fst : A ; snd : B }.
Infix "*" := prod : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing).
Check ltac:({ (1, 1) with {| snd := 2 |} }).
Fail Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type"; should succeed *)
|
