Getting started
Hello, world
Define a function and print its result from main.
Open Hello.lean in editor-- Define a greeting function and run it from main.
def greet (name : String) : String :=
s!"Hello, {name}!"
def main : IO Unit := do
IO.println (greet "world")
IO.println "Welcome to leanlab."
Explanation
def
Introduces a definition. Here, greet is a function and main is the program’s entry point.
(name : String)
A parameter and its type. This function accepts a string named name.
: String :=
The return type comes after a colon. The expression after := supplies the value.
s!"…{name}…"
String interpolation inserts the value of name into the greeting.
IO Unit
An IO action that returns Unit, a type with the single value ().
do
Sequences actions. Indentation groups the two lines into one program.
Expected output
Reference only. Run the file to check its actual result.
Hello, world! Welcome to leanlab.
Exercise
Change "world" to your name, then run the program again.