In Lean, definitions are introduced using the
def keyword. For instance, to define the name
hello to refer to the string
def hello := "Hello"
In Lean, new names are defined using the colon-equal operator
=. This is because
= is used to describe equalities
between existing expressions, and using two different operators helps
In the definition of
hello, the expression
"Hello" is simple enough that Lean is able to determine the definition's type automatically.
However, most definitions are not so simple, so it will usually be necessary to add a type.
This is done using a colon after the name being defined.
def lean : String := "Lean"
Now that the names have been defined, they can be used, so
#eval String.append hello (String.append " " lean)
In Lean, defined names may only be used after their definitions.
In many languages, definitions of functions use a different syntax than definitions of other values.
For instance, Python function definitions begin with the
def keyword, while other definitions are defined with an equals sign.
In Lean, functions are defined using the same
def keyword as other values.
Nonetheless, definitions such as
hello introduce names that refer directly to their values, rather than to zero-argument functions that return equivalent results each time they are called.
There are a variety of ways to define functions in Lean. The simplest is to place the function's arguments before the definition's type, separated by spaces. For instance, a function that adds one to its argument can be written:
def add1 (n : Nat) : Nat := n + 1
Testing this function with
8, as expected:
#eval add1 7
Just as functions are applied to multiple arguments just by writing spaces between each argument, functions that accept multiple arguments are defined with spaces between the arguments' names and types. The function
maximum, whose result is equal to the greatest of its two arguments, takes two
k and returns a
def maximum (n : Nat) (k : Nat) : Nat := if n < k then k else n
When a defined function like
maximum has been provided with its arguments, the result is determined by first replacing the argument names with the provided values in the body, and then evaluating the resulting body. For example:
maximum (5 + 8) (2 * 7) ===> maximum 13 14 ===> if 13 < 14 then 14 else 13 ===> 14
Expressions that evaluate to natural numbers, integers, and strings have types that say this (
String, respectively). This is also true of functions. A function that accepts a
Nat and returns a
Bool has type
Nat → Bool, and a function that accepts two
Nats and returns a
Nat has type
Nat → Nat → Nat.
#check add1 yields
add1 : Nat → Nat and
#check maximum yields
maximum : Nat → Nat → Nat.
This arrow can also be written with an ASCII alternative arrow
->, so the preceding function types can be written
Nat -> Bool and
Nat -> Nat -> Nat, respectively.
Behind the scenes, all functions actually expect precisely one argument.
maximum that seem to take more than one argument are in fact functions that take one argument and then return a new function.
This new function takes the next argument, and the process continues until no more arguments are expected.
This can be seen by providing one argument to a multiple-argument function:
#check maximum 3 yields
maximum 3 : Nat → Nat and
#check String.append "Hello " yields
String.append "Hello " : String → String.
Using a function that returns a function to implement multiple-argument functions is called currying after the mathematician Haskell Curry.
Function arrows associate to the right, which means that
Nat → Nat → Nat should be parenthesized
Nat → (Nat → Nat).
- Define the function
String -> String -> String -> Stringthat creates a new string by placing its first argument between its second and third arguments.
joinStringsWith ", " "one" "and another"should evaluate to
"one, and another".
- What is the type of
joinStringsWith ": "? Check your answer with Lean.
- Define a function
Nat → Nat → Nat → Natthat computes the volume of a rectangular prism with the given height, width, and depth.
Most typed programming languages have some means of defining aliases for types, such as C's
In Lean, however, types are a first-class part of the language - they are expressions like any other.
This means that definitions can refer to types just as well as they can refer to other values.
For instance, if
String is too much to type, a shorter abbreviation
Str can be defined:
def Str : Type := String
It is then possible to use
Str as a definition's type instead of
def aStr : Str := "This is a string."
The reason this works is that types follow the same rules as the rest of Lean.
Types are expressions, and in an expression, a defined name can be replaced with its definition.
Str has been defined to mean
String, the definition of
aStr makes sense.
Experimenting with using definitions for types is made more complicated by a feature of Lean that has not yet been introduced.
Nat is too short, a longer name
NaturalNumber can be defined:
def NaturalNumber : Type := Nat
NaturalNumber as a definition's type instead of
Nat does not have the expected effect.
In particular, the definition:
def thirtyEight : NaturalNumber := 38
results in the following error:
failed to synthesize instance OfNat NaturalNumber 38
This error occurs because Lean allows number literals to be overloaded. When it makes sense to do so, natural number literals can be used for new types, just as if those types were built in to the system. This is part of Lean's mission of making it convenient to represent mathematics, and different branches of mathematics use number notation for very different purposes. The specific feature that allows this overloading does not replace all defined names with their definitions before looking for overloading, which is what leads to the error message above.
One way to work around this limitation is by providing the type
Nat on the right-hand side of the definition, causing
Nat's overloading rules to be used for
def thirtyEight : NaturalNumber := (38 : Nat)
The definition is still type-correct because
NaturalNumber is the same type as
Another solution is to define an overloading for
NaturalNumber that works equivalently to the one for
This requires more advanced features of Lean, however.
Finally, defining the new name for
abbrev instead of
def allows overloading resolution to replace the defined name with its definition.
Definitions written using
abbrev are always unfolded.
abbrev N : Type := Nat
def thirtyNine : N := 39
are accepted without issue.
Behind the scenes, some definitions are internally marked as being unfoldable during overload resolution, while others are not.
Definitions that are to be unfolded are called reducible.
Control over reducibility is essential to allow Lean to scale: fully unfolding all definitions can result in very large types that are slow for a machine to process and difficult for users to understand.
Definitions produced with
abbrev are marked as reducible.