Zulip Chat Archive

Stream: new members

Topic: Demos in introduction


view this post on Zulip Buster (Mar 25 2021 at 15:49):

I'm reading the introduction and looking at the first "try_it!" link. After a while, 'Lean is busy' changes to 'Lean is ready', but there isn't any output: I can click on expressions to see their types, but it doesn't produce a proof. Is it supposed to? Just trying to get my bearings before I read too much further. :smile:

view this post on Zulip Bryan Gin-ge Chen (Mar 25 2021 at 15:55):

I think this is expected. If you edit the proof randomly, it should break and you should get some errors.

view this post on Zulip Buster (Mar 25 2021 at 15:56):

Ah, thanks! It's already a proof, and running Lean checks it, right?

view this post on Zulip Bryan Gin-ge Chen (Mar 25 2021 at 15:57):

Yes, that's correct.


Last updated: May 11 2021 at 12:15 UTC