Stream: new members
Topic: Demos in introduction
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:
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.
Buster (Mar 25 2021 at 15:56):
Ah, thanks! It's already a proof, and running Lean checks it, right?
Bryan Gin-ge Chen (Mar 25 2021 at 15:57):
Yes, that's correct.
Last updated: May 11 2021 at 12:15 UTC