Demos in introduction

Stream: new members

[Buster]

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]

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

[Buster]

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

[Bryan Gin-ge Chen]

Yes, that's correct.