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