blob: 13de4bca84f521415d3d1f81729cfb4cdd996b69 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Require Import mathcomp.ssreflect.ssreflect.
Tactic Notation "at" ssrpatternarg(p) tactic(t)
:=
ssrpattern p; let top := fresh in intro top;
t top; try unfold top in * |- *; try clear top.
Goal forall x y, x + y = 4.
intros.
at [RHS] (fun top => remember top as E eqn:E_def).
match goal with
| |- x + y = E => idtac
| |- _ => fail
end.
Admitted.
|
