Zulip Chat Archive

Stream: general

Topic: Better check


Patrick Massot (Nov 03 2021 at 14:21):

It would be nice to have a user command #state foo that does the same work as #check @foo but displays as much as possible left of colon, replace all Type u_N by Type* and all [_inst_N : bar] by [bar]. The use case is when I want to create a lemma that has almost the same assumptions than foo.

Eric Wieser (Nov 03 2021 at 15:09):

Presumably this shouldn't be too hard, since essentially doc-gen does it

Patrick Massot (Nov 03 2021 at 15:15):

Yes, I very much hope someone will be able to do it easily. But I don't want to put pressure on any specific inhabitant of Providence.


Last updated: Dec 20 2023 at 11:08 UTC