Stream: math-comp users

Topic: Syntax for reverse in multirule rewrite


view this post on Zulip Laurent Théry (Feb 26 2024 at 13:40):

I keep forgetting what is the syntax to reverse an element in a multirule. The doc seems to indicate that the syntax is

rewrite (=~ multi1)

but this gives me a syntax error, what I am missing?

view this post on Zulip Cyril Cohen (Feb 26 2024 at 13:57):

There seem to be a vanishing hat... :top_hat:

view this post on Zulip Cyril Cohen (Feb 26 2024 at 13:57):

should be (=^~multi1)

view this post on Zulip Laurent Théry (Feb 26 2024 at 13:57):

thanks I will make a PR in the doc

view this post on Zulip Cyril Cohen (Feb 26 2024 at 13:58):

cf https://github.com/coq/coq/blob/954e315d0026c2c0f02babc3bea7932dcd590837/theories/ssr/ssreflect.v#L37-L38

view this post on Zulip Laurent Théry (Feb 26 2024 at 13:59):

hard to remember.....

view this post on Zulip Cyril Cohen (Feb 26 2024 at 13:59):

yes

view this post on Zulip Cyril Cohen (Feb 26 2024 at 14:00):

I guess a right to left arrow would be welcome

view this post on Zulip Cyril Cohen (Feb 26 2024 at 14:00):

(at least as an alias)


Last updated: Jul 25 2024 at 15:02 UTC