Zulip Chat Archive
Stream: general
Topic: attribute [congr] dif_ctx_congr
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 simp
.
Scott Morrison (Jul 02 2020 at 05:20):
and mathlib compiles fine. I guess I better PR to core.
Last updated: May 02 2025 at 03:31 UTC