Zulip Chat Archive

Stream: new members

Topic: Doing #check inside a proof


view this post on Zulip Jakob Scholbach (Mar 17 2021 at 18:53):

Is there a way to use #check inside a proof? Or some other way to "debug" what a certain expression is?

view this post on Zulip Patrick Massot (Mar 17 2021 at 18:54):

use have or let

view this post on Zulip Johan Commelin (Mar 17 2021 at 18:54):

@Jakob Scholbach If you are using VScode, you can also click on expressions in the goal window to get more info.

view this post on Zulip Johan Commelin (Mar 17 2021 at 18:54):

But this only works if you don't have an error.

view this post on Zulip Jakob Scholbach (Mar 17 2021 at 19:04):

Yes, @Johan Commelin I was aware of clicking at things, but my problem was / is that I often need to figure out why I can't invoke some theorem in some specific way. But @Patrick Massot s advice is helpful, merci bien!


Last updated: May 08 2021 at 10:12 UTC