leanprover
Setup Guide should say something about running resulting executables
After creating my project using lake new my_project, it took a bit of searching to figure out that I can use lake env lean --run Main.lean to call the main definition and get "Hello, world!" printed to the console. At first I read this https://lean-lang.org/functional_programming_in_lean/hello-world/running-a-program.html and it said there that you can use lean --run Main.lean to run the program but that did not work for me because by default it seems that lean does not search the current directory for modules.
Later I also found out here https://lean-lang.org/functional_programming_in_lean/hello-world/starting-a-project.html that it is possible to use lake exe my_project to build and run the program.
