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.

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.

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."

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)

Other Useful Commands

Beyond #eval and #check, Lean offers additional introspection tools that help you understand existing definitions.

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

#eval vs #reduce

Both commands evaluate expressions, but they work differently:

1-- #eval: fast, practical
2#eval 2 ^ 100    -- Instant result
3
4-- #reduce: kernel-level, trusted
5#reduce 2 + 2    -- 4 (computed by the trusted kernel)
6
7-- #eval can do IO
8#eval IO.println "Hello"  -- Prints to infoview
9
10-- #reduce cannot
11-- #reduce IO.println "Hello"  -- Error!

Understanding Error Messages

Lean's error messages are detailed and helpful. Here's how to read them:

1-- Type mismatch example
2def badAdd : Nat := "hello"
3-- Error: type mismatch
4--   "hello"
5-- has type
6--   String
7-- but is expected to have type
8--   Nat

Error messages typically show: what you provided (in this case "hello"), its type (String), and what was expected (Nat).

1-- Unknown identifier
2#eval unknownFunction 5
3-- Error: unknown identifier 'unknownFunction'
4
5-- Application type mismatch
6#eval String.length 42
7-- Error: application type mismatch
8--   String.length 42
9-- argument
10--   42
11-- has type
12--   Nat : Type
13-- but is expected to have type
14--   String : Type

Practice the Loop

The fastest way to learn Lean is a tight feedback loop: write a line, check a type, evaluate a value, and adjust. This exercise builds that habit.

1def greeting := "Hello, Lean!"
2
3#check greeting
4#eval greeting

Your First File

Create a file called Hello.lean and add:

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.