Tactic Notation"at""[" ssrpatternarg(pat) "]" tactic(t) := let name := fresh in let def_name := fresh in
ssrpattern pat; intro name; poseproof (refl_equal name) as def_name; unfold name at 1 in def_name;
t def_name;
[ rewrite <- def_name | idtac.. ];
clear name def_name.
Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4. Proof.
at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place).
- reflexivity.
- trivial.
- trivial. Qed.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
