Zulip Chat Archive
Stream: mathlib4
Topic: Deprecated defs
Moritz Doll (Sep 16 2022 at 02:55):
I found instances of getLocalDecl which is marked as deprecated, are PRs that replace those welcome?
Mario Carneiro (Sep 16 2022 at 03:06):
yes
Mario Carneiro (Sep 16 2022 at 03:06):
I'm not sure why these aren't triggering CI
Moritz Doll (Sep 16 2022 at 03:39):
mathlib4#418 but I have probably not found all
Moritz Doll (Sep 16 2022 at 03:39):
(duplicate)
Last updated: Dec 20 2023 at 11:08 UTC