Stream: Equations devs & users

Topic: Equations incompatible with mathematical components?


view this post on Zulip Yves Bertot (May 25 2021 at 14:11):

Has anyone tried to use Equations and mathematical components at the same time? A first issue I encounter is because of eq_refl change of arguments. But it seems the rewrite with multi-rules also does not work.

view this post on Zulip Matthieu Sozeau (May 26 2021 at 10:11):

We use them both in MetaCoq. rewrite and multi-rewrites work, but until Equations 1.2.4 there was a parsing conflict when using -!

view this post on Zulip Paolo Giarrusso (May 26 2021 at 21:52):

wait, was that fixed by adding a space (-! -> - !) like rewrite - !lemma? We've wondered about that for months...

view this post on Zulip Paolo Giarrusso (May 26 2021 at 21:53):

(okay we wondered a tiny bit and I refrained from investigating, I was just very flabbergasted)

view this post on Zulip Matthieu Sozeau (May 27 2021 at 10:42):

Yes, the fix before was to add a space. This is no longer needed

view this post on Zulip Matthieu Sozeau (May 27 2021 at 10:43):

I've been annoyed with this for quite some time too ;)


Last updated: Jan 29 2023 at 14:02 UTC