Zulip Chat Archive

Stream: new members

Topic: How to run Lean programs from the command line


view this post on Zulip Juan Pablo Romero (Mar 30 2021 at 16:38):

Hi, can anyone point me to the docs showing how to run Lean 3/4 programs from the command line?

view this post on Zulip Alex J. Best (Mar 30 2021 at 16:48):

https://agentultra.github.io/lean-for-hackers/ might be what you are looking for for lean 3

view this post on Zulip Juan Pablo Romero (Mar 30 2021 at 17:01):

Ah, thanks!

Somehow I missed the rather obvious lean --run hello.lean


Last updated: May 13 2021 at 19:20 UTC