Programming · 8 min
Programs and IO
A Lean program has a main declaration. The type IO Unit describes an action that may perform input/output and finishes without a meaningful value. IO.println prints a line; do sequences several actions.
In this browser, Run program evaluates main with Lean’s #eval command in an isolated worker. On your computer, lean --run Main.lean runs main. A Lake executable target can compile the same program into a native binary.
Exercise
Define greeting as "Hello, Lean!", then run the main program that prints it.
Open exercise in editordef greeting : String := "Hello"
def main : IO Unit := do
IO.println greeting
Hint
Change the string assigned to greeting. Run program executes the supplied main action.
Solution
def greeting : String := "Hello, Lean!"
def main : IO Unit := do
IO.println greeting