Is it possible to define some small tactic script and then reuse it during the proof but not letting it go out of the scope of the proof. I'm looking for something like
Lemma foo x : y.
Proof.
let _easy := match goal with ... end in
destruct v; try _easy.
{ blablabla; _easy. }
{ otherblablaba; _easy. }
Qed.
The let _easy := ... in
works until I put a {
, is there any alternative for that?
Qed.
clears any tactics, but a section's End
does — so you can wrap your lemma into Section foo. .... End foo.
let
works until .
, not {
.Yeah but I have to add .
before {
, so ... I can use [foo|bar]
but is not as convenient as {...}
ah I was unclear: I agree, I do mean that let
lasts even less
Last updated: Oct 13 2024 at 01:02 UTC