Lambda Functions

Anonymous Functions (Lambdas)

In Lean, you can create functions without naming them using fun:

fun x => x * 2

This creates a function that takes x and returns x * 2. You can assign it to a name:

def double := fun (x : Nat) => x * 2

#eval double 7    -- 14

Lambdas with multiple parameters:

def add := fun (x y : Nat) => x + y

#eval add 3 4    -- 7

Lambdas are most useful when you need to pass a function as an argument (which we will see in the next lessons).

Your Turn

Define square as a lambda that squares a number, and negate as a lambda that subtracts a number from 10.