Scott Morrison (Jul 02 2020 at 04:42):
Is there any reason that
dif_ctx_congr is not marked as
@[congr]? It really does work with
Scott Morrison (Jul 02 2020 at 05:20):
and mathlib compiles fine. I guess I better PR to core.
Last updated: May 17 2021 at 22:15 UTC