# 1.4 Basic Syntax and Expressions

Lean code is built from expressions. An expression may be a value, a function, a type, a proposition, or a proof. The same syntactic system is used for computation and reasoning, so learning the basic expression language is the first step toward writing both programs and theorems.

## Problem

You want to read and write small Lean expressions, understand their types, and recognize how Lean parses ordinary definitions and proof terms.

## Solution

Use `#check` to inspect the type of an expression and `#eval` to compute expressions that have executable content.

```lean id="xv9s8a"
#check 5
#check Nat
#check String
#check true
#check fun x : Nat => x + 1

#eval 5 + 7
#eval "Lean" ++ " " ++ "Cookbook"
#eval (fun x : Nat => x + 1) 10
```

Typical output includes types such as:

```text id="40ahka"
5 : Nat
Nat : Type
String : Type
true : Bool
fun x => x + 1 : Nat -> Nat
12
"Lean Cookbook"
11
```

The command `#check` asks Lean to infer a type. The command `#eval` asks Lean to compute a value.

## Expressions

An expression is any Lean term that can be checked by the type system.

Examples:

```lean id="66qg4r"
42
"hello"
true
Nat
Nat -> Nat
fun x : Nat => x + 1
```

Each expression has a type.

```lean id="x6a580"
#check 42              -- 42 : Nat
#check "hello"         -- "hello" : String
#check true            -- true : Bool
#check Nat             -- Nat : Type
#check Nat -> Nat      -- Nat -> Nat : Type
```

Types themselves are expressions. For example, `Nat` has type `Type`.

## Function Application

Function application is written by placing the argument after the function.

```lean id="3jtw3u"
#eval Nat.succ 4
```

The result is:

```text id="0nd70q"
5
```

Multiple arguments are written by placing them in sequence:

```lean id="omkw8a"
#eval Nat.add 3 4
```

This means:

```lean id="jmlt5b"
(Nat.add 3) 4
```

Function application associates to the left. Therefore:

```lean id="tptn23"
f x y z
```

means:

```lean id="e1kgbc"
(((f x) y) z)
```

## Function Types

The type:

```lean id="6dmire"
Nat -> Nat
```

means a function from natural numbers to natural numbers.

A function with two arguments has a curried type:

```lean id="rg8w6k"
Nat -> Nat -> Nat
```

This means:

```lean id="edymno"
Nat -> (Nat -> Nat)
```

A function takes one argument and returns another function. This convention makes partial application natural.

```lean id="2shmg1"
def addThree : Nat -> Nat -> Nat :=
  fun x y => x + y + 3

#check addThree
#check addThree 4
#eval addThree 4 5
```

The expression `addThree 4` is itself a function.

## Lambda Expressions

A lambda expression creates an anonymous function.

```lean id="5k28mp"
fun x : Nat => x + 1
```

This expression has type:

```lean id="25sje5"
Nat -> Nat
```

Several arguments can be written together:

```lean id="n9pl6t"
fun x y : Nat => x + y
```

This is shorthand for:

```lean id="j1y903"
fun x : Nat => fun y : Nat => x + y
```

Lambda expressions are useful when a small function is needed only once.

```lean id="j1zi7q"
#eval List.map (fun x : Nat => x + 1) [1, 2, 3]
```

Expected result:

```text id="bn55xh"
[2, 3, 4]
```

## Let Expressions

A `let` expression gives a local name to a value.

```lean id="htvvzl"
#eval
  let x := 10
  let y := 20
  x + y
```

Expected result:

```text id="hkcx1f"
30
```

A `let` expression is still an expression. It computes by replacing the local name with its value.

You can also annotate the type:

```lean id="0sg3r9"
#eval
  let x : Nat := 10
  x + 5
```

Annotations are useful when Lean cannot infer the intended type.

## Parentheses

Parentheses control parsing.

```lean id="893m5w"
#eval (fun x : Nat => x + 1) 5
```

Without parentheses, Lean would try to parse the expression differently.

Parentheses are also useful in nested applications:

```lean id="471pjg"
#eval Nat.succ (Nat.succ 3)
```

Expected result:

```text id="iuh2c6"
5
```

## Infix Operators

Many functions have infix notation.

```lean id="7e9tjs"
#eval 2 + 3
#eval 10 - 4
#eval 3 * 5
```

These are notation for ordinary functions. For example:

```lean id="8vrcrk"
2 + 3
```

is notation for addition on natural numbers.

Precedence determines how expressions are grouped.

```lean id="wi0v10"
#eval 2 + 3 * 4
#eval (2 + 3) * 4
```

Expected results:

```text id="4g1ige"
14
20
```

## Type Ascription

A type ascription tells Lean the intended type of an expression.

```lean id="cdw08m"
#check (5 : Nat)
#check ("hello" : String)
```

This is useful when literals are overloaded.

```lean id="kgo2do"
#check (0 : Nat)
#check (0 : Int)
```

The same printed literal may be elaborated at different types, depending on context.

## Propositions as Expressions

Propositions are also expressions.

```lean id="tx9dms"
#check True
#check False
#check 1 = 1
#check Nat
```

Typical output:

```text id="tphxnu"
True : Prop
False : Prop
1 = 1 : Prop
Nat : Type
```

A proof is an expression whose type is a proposition.

```lean id="166k9x"
#check True.intro
#check rfl
```

The term `True.intro` proves `True`. The term `rfl` proves equalities that hold by reflexivity or definitional computation.

## Definitions

A definition binds a name to an expression.

```lean id="f56up6"
def one : Nat :=
  1

def two : Nat :=
  one + one
```

After these declarations, the names can be checked and evaluated.

```lean id="spctjb"
#check one
#eval two
```

Expected result:

```text id="qzp9vr"
2
```

The general shape is:

```lean id="4g16ii"
def name : Type :=
  expression
```

Lean checks that `expression` has the declared type.

## Theorems as Expressions

A theorem binds a name to a proof expression.

```lean id="l0gq07"
theorem true_example : True :=
  True.intro
```

The general shape is:

```lean id="w0gmlo"
theorem name : proposition :=
  proof
```

A theorem is checked like any other declaration. The difference is that its declared type lies in `Prop`.

A tactic proof produces the same kind of proof term:

```lean id="wurwfo"
theorem implication_example (P : Prop) : P -> P := by
  intro h
  exact h
```

This theorem says that every proposition implies itself.

## Holes

A hole asks Lean to report what it needs at that point.

```lean id="bht3x7"
def addOne (n : Nat) : Nat :=
  _
```

Lean reports that the hole has expected type `Nat`.

Holes are useful during development because they reveal the local context and the target type.

A named hole can appear more than once:

```lean id="y67ze1"
def pairSame (n : Nat) : Nat × Nat :=
  (?x, ?x)
```

Lean reports a goal named `?x`.

## Commands vs Expressions

Some Lean syntax is a command, not an expression.

Commands include:

```lean id="gqrtiu"
def
theorem
#check
#eval
import
namespace
end
```

Expressions include:

```lean id="103s6q"
5
Nat
fun x : Nat => x + 1
x + y
True
```

Commands modify or inspect the environment. Expressions are the terms that Lean checks.

## Recipe: Inspect Before You Prove

When a proof or definition fails, inspect smaller pieces.

```lean id="1ri16r"
#check Nat.succ
#check Nat.succ 3
#eval Nat.succ 3
```

Then build the final declaration:

```lean id="7tzu9y"
def next (n : Nat) : Nat :=
  Nat.succ n
```

This style avoids guessing. Lean becomes easier to use when each subexpression has a known type.

## Common Pitfalls

If Lean reports a type mismatch, insert a type ascription to make the intended type explicit.

If function application parses incorrectly, add parentheses.

If a literal has the wrong type, annotate it.

If a name is unknown, check imports and namespaces.

If a theorem looks like a definition, remember that the difference is its type: propositions live in `Prop`.

## Takeaway

Lean programs and proofs are built from expressions. Every expression has a type, and types themselves are expressions. Function application, lambda abstraction, let binding, type ascription, and proposition formation are the basic forms you need before definitions, theorems, tactics, and larger modules become predictable.