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: Jun 10 2023 at 23:01 UTC