Stream: Coq users

Topic: ✔ Is it possible to make assert transparent?

view this post on Zulip Daniel Hilst Selli (Jun 21 2022 at 12:30):

Oh, I didn't know about unshelve eexists thanks, cool!

view this post on Zulip Notification Bot (Jun 21 2022 at 12:30):

Daniel Hilst Selli has marked this topic as resolved.

view this post on Zulip Daniel Hilst Selli (Jun 21 2022 at 13:34):

Oh I can do unshelve eassert (2 * x = _ x) and get a subgoal focused for this hole

Last updated: Feb 09 2023 at 00:03 UTC