Module 1 · Lesson 1

The Environment

Lean 4 is a compiled language with a uniquely interactive development experience. Before writing your first program, let's understand the tools you'll use every day.

Interactive Evaluation with #eval

Unlike traditional compiled languages where you write code, compile, and run, Lean provides immediate feedback through the #eval command. This evaluates expressions directly in your editor and shows the result.

lean

1-- Evaluate simple expressions
2#eval 1 + 1           -- Output: 2
3#eval "Hello" ++ "!"  -- Output: "Hello!"
4#eval 2 ^ 10          -- Output: 1024
5
6-- Evaluate function calls
7#eval String.length "Lean 4"  -- Output: 6
8#eval List.reverse [1, 2, 3]  -- Output: [3, 2, 1]

The result appears in your editor's "Lean Infoview" panel (in VS Code) or inline as a comment. This makes exploration and learning incredibly fast—you never need to leave your editor.

Type Inspection with #check

While #eval runs code, #check reveals types. This is essential for understanding what you're working with.

lean

1#check "Hello World"   -- String
2#check 42              -- Nat
3#check true            -- Bool
4#check [1, 2, 3]       -- List Nat
5
6-- Check function types
7#check String.length   -- String → Nat
8#check List.reverse    -- {α : Type} → List α → List α

Notice the arrow → in function types. This reads as "takes X and returns Y." For example, String → Nat means "a function that takes a String and returns a Nat."

Key Takeaway

#eval executes code and shows results. #check shows the type without executing. Use both constantly as you learn—they're your primary debugging tools.

The Infoview Panel

In VS Code with the Lean 4 extension, the Infoview panel is your companion. It shows:

Results from #eval and #check
Type information when you hover over expressions
Error messages with detailed explanations
Goal state when writing proofs (covered in Tactics)

💡

Position your cursor on any expression and the Infoview will show its type. This is faster than writing #check everywhere.

Other Useful Commands

Lean provides several other inspection commands:

lean

1-- Print the definition of something
2#print Nat.add
3
4-- Reduce an expression step by step
5#reduce 2 + 2
6
7-- Search for functions by type (requires Mathlib)
8-- #check @?_ : Nat → Nat → Nat

Deep Dive: Compiled vs Interpreted

When you run a Lean program as an executable, it compiles to efficient C code and then to native machine code. However, #eval runs in an interpreter for immediate feedback.

This means #eval is great for learning and debugging, but performance-critical code should be tested with actual compilation usinglake build.

Your First File

Create a file called Hello.lean and add:

lean|Hello.lean

1-- My first Lean file
2#eval "Hello, Lean 4!"
3
4-- Check some types
5#check Nat
6#check String → Bool
7
8-- A simple definition (we'll cover this next)
9def greeting := "Welcome to Lean!"

Save the file and watch the Infoview update. You should see "Hello, Lean 4!" appear as the result of the #eval.

Module 1: Foundations

Next: Primitives & Basic Types