Zulip Chat Archive
Stream: lean4
Topic: Lean.ConstantInfo.all strangeness
Arthur Paulino (Aug 19 2022 at 19:43):
We noticed a case in which the .all attribute came with the wrong name for a definition. One ended with overwrite and the other didn't. Why does that happen?
Arthur Paulino (Aug 23 2022 at 14:27):
:ping_pong: because I had posted this on a weekend.
Also CC'ing @Rish Vaishnav
Last updated: Dec 20 2023 at 11:08 UTC