λleanlab

Getting started

Writing functions

Functions take inputs and return values. Application uses spaces, so parentheses group expressions.

Open Functions.lean in editor
def double (n : Nat) : Nat :=
  n * 2

def add (a b : Nat) : Nat :=
  a + b

def main : IO Unit := do
  IO.println (double 21)
  IO.println (add 10 32)
  IO.println (double (add 3 4))

Explanation

Nat

The natural numbers: 0, 1, 2, and so on. Nat has no negative values.

(a b : Nat)

Two parameters sharing the same type.

double (add 3 4)

Calls add first, then passes the result to double. Function arguments are separated by spaces.

Expected output

Reference only. Run the file to check its actual result.

42
42
14

Exercise

Define triple, then print triple (double 7).