Julien Puydt (Nov 11 2022 at 13:28): Julien Puydt (Nov 11 2022 at 13:28):I know ring cannot be used in rewrite because it's a tactic and not a result, but I noticed that I sometimes end up arguing:
have H: ... = ... by ring.
rewrite H.
clear H.
which is basically emulating that behaviour ; but introducing a named hypothesis just to drop it seems a bit ugly.
Perhaps there's a more elegant way to proceed?
Pierre Jouvelot (Nov 11 2022 at 13:42):Isnt have -> : ... = ... working for this?
Envoye depuis mon mobile.
Julien Puydt (Nov 11 2022 at 13:53):Yes! That helps. It doesn't work for rewrite {2}H, but I guess there something smart with which to replace "->" and get it?
Julien Puydt (Nov 11 2022 at 13:59):have {2}->: ... = ...does the trick.
@Pierre Jouvelot thanks!
Notification Bot (Nov 11 2022 at 13:59):Julien Puydt has marked this topic as resolved.
Enrico Tassi (Nov 11 2022 at 15:23):see also rewrite (_ : ... = ...)
Julien Puydt (Nov 11 2022 at 15:39):Oh, I like that one - even though it's used more rarely according to my grep's result.
Last updated: Feb 02 2023 at 15:04 UTC