Stream: math-comp users

Topic: ✔ Rewrite with ring


view this post on Zulip 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?

view this post on Zulip Pierre Jouvelot (Nov 11 2022 at 13:42):

Isnt have -> : ... = ... working for this?

Envoye depuis mon mobile.

view this post on Zulip 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?

view this post on Zulip Julien Puydt (Nov 11 2022 at 13:59):

have {2}->: ... = ...does the trick.

@Pierre Jouvelot thanks!

view this post on Zulip Notification Bot (Nov 11 2022 at 13:59):

Julien Puydt has marked this topic as resolved.

view this post on Zulip Enrico Tassi (Nov 11 2022 at 15:23):

see also rewrite (_ : ... = ...)

view this post on Zulip 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