Zulip Chat Archive
Stream: mathlib4
Topic: simpa? "Try this" not clickable
Michael Stoll (Nov 04 2023 at 15:00):
See thread title. Using simpa? using <blah> gives a suggestion "Try this: simpa only [...] using <blah>" in the infoview, but it cannot be clicked to be copied into the code.
Kyle Miller (Nov 04 2023 at 17:41):
Last updated: Dec 20 2023 at 11:08 UTC