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.
We use them both in MetaCoq. rewrite
and multi-rewrites work, but until Equations 1.2.4 there was a parsing conflict when using -!
wait, was that fixed by adding a space (-!
-> - !
) like rewrite - !lemma
? We've wondered about that for months...
(okay we wondered a tiny bit and I refrained from investigating, I was just very flabbergasted)
Yes, the fix before was to add a space. This is no longer needed
I've been annoyed with this for quite some time too ;)
Last updated: Oct 13 2024 at 01:02 UTC