The Lean Context

• "Everything" in Lean is a term. Terms have types.
• Terms include:
  • numbers, strings
  • functions
  • lists
  • propositions (logical statements)
  • proofs
  • types
• We can form expressions for terms and types.
• We make two kinds of judgements:
  • term a has type α.
  • terms a and b are equal by definition.
• The context has terms with names.

Simple Terms and Types

We consider a few terms and types in Lean. These are definitions that do not involve recursion/induction or propositions.

The #check command displays the type of a term.

def two : Nat

Equations

• two = 2

def five : Nat

Equations

• five = two + 3

Function types

If α and β are types, then α → β is the type of functions from α to β.

def cube (n : Nat) : Nat

The cube of a natural number.

Equations

• cube n = n * n * n

def cubeGeneric {α : Type} [Mul α] (n : α) : α

A generic function to compute the cube of a number. This defines the cube for a type α with a multiplication operation.

Equations

• cubeGeneric n = n * n * n

def myMul : Mul Int

Equations

• myMul = { mul := fun (m n : Int) => m + n }

def cube' : Nat → Nat

The cube of a natural number, using a lambda expression.

Equations

• cube' n = n * n * n

def cube'' (n : Nat) : Nat

The cube of a natural number, using a lambda expression with argument type specified.

Equations

• cube'' n = n * n * n

Curried functions

Suppose we want to define the function f of two variables a and b taking value a + b + 1. We can define it as a function of one variable a returning a function of one variable b.

def sum_of_squares : Nat → Nat → Nat

The function of two variables a and b taking value a * a + b * b, defined as an iterated lambda.

Equations

• sum_of_squares a b = a * a + b * b

def sum_of_squares' (a b : Nat) : Nat

The function of two variables a and b taking value a * a + b * b, using arguments in a single pair of parentheses.

Equations

• sum_of_squares' a b = a * a + b * b

def sum_of_squares'' : Nat → Nat → Nat

The function of two variables a and b taking value a * a + b * b, using a lambda expression with two arguments.

Equations

• sum_of_squares'' a b = a * a + b * b

def sum_of_squares''' (a b : Nat) : Nat

The function of two variables a and b taking value a * a + b * b, using a lambda expression with two arguments and type annotations for one. The other type is inferred.

Equations

• sum_of_squares''' a b = a * a + b * b

We used typeclasses above. We will discuss them later. For now, note that they are simply types or type families. However, there are plenty of type families that are not typeclasses.

Implicit parameters

A function parameter may be implicit. This means that it is inferred by Lean from consistency of types. We can make a parameter implicit by enclosing it in curly braces {}.

A typeclass parameter is always implicit.

If we prefix a function application with @, then we must provide all implicit parameters explicitly. Conversely, we can use _ for an explicit parameter to make it implicit.

def doubleList {α : Type} (l : List α) : List α

Equations

• doubleList l = l ++ l

When calling the function doubleList, we give only one argument, the list l. The type α is inferred from the type of l.

def doubleList' (α : Type) (l : List α) : List α

Equations

• doubleList' α l = l ++ l

When calling the function doubleList', we must provide the type α explicitly.

When calling, we can make all parameters explicit or leave some explicit parameters to be deduced.

def doubleList''' {α : Type} (l : List α) : List α

Equations

• doubleList''' l = l ++ l

def doubleList'' {α : Type u_1} (l : List α) : {α✝ : Type} → List α

Equations

• doubleList'' l = l ++ l