Syllabus

Basic Lean4 syntax

This page contains generic information about basic Lean4 syntax. It is intended as a very quick introduction, just to get you started. It is in no way meant to be comprehensive, but is mostly so that you can follow along some of the code. In my opinion, the best way to learn is to play yourself with the code, modify it, stretch it to its limits, try to make it do weird things!

Text that Lean4 does not parse

Single comments, beginning with -- and ending at the following line break.
```
-- I am a comment
```
Comment blocks, beginning with /- and ending with -/, possibly spanning several lines.
```
/-
I am a longer comment.
I may span multiple lines.
-/
```
Doc-strings, beginning with /-- and ending with -/, possibly spanning several lines. They produce “hover information” about the declaration that follows them.
```
/-- I usually say something meaningful about the function that follows me.
I appear when you hover over the definition that follows me. -/
```
Doc-modules, beginning with /-! and ending with -/, possibly spanning several lines. For the purpose of this repository, they behave just like comments. In more automated projects, such as mathlib, doc-module strings appear in the autogenerated documentation pages, while regular comments do not.
```
/-! I usually say something meaningful about the overall structure or declarations in a file.
I do not appear on hover and I am essentially indistinguishable from a comment in this repository. -/
```

Text that Lean4 parses

The bulk of each file consists of definitions.

def myFn <inputs> : <target> := <whatTheFunctionDoes>

Usually once per file, you will find namespace <name> (and <name> is often Day<number>, though List, String and Array are also common). This indicates that if the remaining code defines a function myFn, then its actual full name is Day<number>.myFn. Within the namespace, you can simply call myFn and Lean4 will add Day<number>. for you automatically (unless, of course, there is some ambiguity that it cannot resolve). namespace <name> ends with the line end <name> or with the end of the file.

The command open <name> means that you can refer to <name>.myFn simply as myFn, even if you are not within namespace <name>.

Thus, in the following code, the second def fn defines fn. Note that, if the first fn had not been inside a namespace, then there would have been a clash of names and Lean4 would have complained.

namespace myName

/-- I describe `myName.fn`. -/
def fn := 0
-- this definition really created `myName.fn`

end myName

/-- I describe `fn`. -/
def fn := 1
-- this definition created `fn`, without namespace

#eval fn  -- 1

open myName

/-
#eval fn
causes an error, since Lean4 cannot know whether we mean `myName.fn` or `fn` with no namespace.
We disambiguate this as follows.
-/

-- if you hover over `myName.fn`, you will see "I describe `myName.fn`."
#eval myName.fn -- 0

-- if you hover over `_root_.fn`, you will see "I describe `fn`."
#eval _root_.fn -- 1
/- `_root_.` is a way of letting Lean4 know that what follows is the full name,
even if we are inside a `namespace`-block. -/

set_option profiler true instructing Lean4 to provide some further information, usually in the form of evaluation time of declarations, #evals,…

Dot-notation

As we have seen, namespaces allow us to “repeat” names of declarations. They also allow us to organize names into common groups, by naming similar definitions in the same namespace.

An interesting feature of namespaces is what is called “dot-notation”. Let us begin with an example.

Suppose that we define a function List.twice as follows.

def List.twice (L : List Nat) : List Nat := L ++ L

#eval List.twice [1,2,3] -- [1,2,3,1,2,3]

Thus, List.twice L creates a list twice as long as L consisting of two copies of L, one after the other. Observe that there is a coincidence: the Type of L is List ... and the name of the declaration is List.[...]. In this situation, we can replace the namespace List with the term L and obtain that List.twice L = L.twice. Of course, this trick cannot work always: there is the need of the coincidence of an argument of a function having a Type that is the namespace of the function itself. Nevertheless, since we choose the namespace, we can get “dot-notation” to work fairly often. This is a further reason why definitions and theorems about Lists are very often in the List namespace: since they apply to Lists, they likely take a term of type List ... as an argument and then dot-notation can be used. In case you are wondering, the shortening can happen also if the function has several arguments: dot-notation allows you to merge the first explicit argument of the correct Type with the namespace of the declaration.

Here is a situation where we can use dot-notation twice. We first generalize the definition of List.twice above to work for lists of arbitrary Types. Next, we take a term of Type String and we apply String.toList to it, converting a String to a list of characters. Finally, we apply List.twice to the resulting list of characters.

/-- For an arbitrary Type `α`, and a list `L : List α`, `List.twice L = L.twice` is the
list obtained by concatenating `L` with itself. -/
def List.twice (L : List α) : List α := L ++ L

#eval String.toList "abc" -- ['a', 'b', 'c'], the list of characters `'a', 'b', 'c'`

#eval "abc".toList -- ['a', 'b', 'c'], same as above, using dot-notation "with `String`"

#eval "abc".toList.twice -- ['a', 'b', 'c', 'a', 'b', 'c'], dot-notation twice!
#eval List.twice (String.toList "abc") -- same as above

Let’s go over the expression "abc".toList.twice again. First, "abc".toList is dot-notation for String.toList "abc" (we know this, since "abc" is a String). Moreover, "abc".toList produces a List, as the name suggests! Thus, if we want to apply List.twice to "abc".toList, we can again take advantage of dot-notation: we can compress it to "abc".toList.twice.

You can find a more extended example here

Back to the Theorem Proving with Lean webpage

Back to the Mathlib project for the module

Back to Moodle

This site is open source. Improve this page.