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: Aug 03 2023 at 10:10 UTC