# Lean, explained the way you'd want it explained

> A hands-on tour of Lean's syntax, from def and #eval to proofs that run at typecheck time.
- Title: Lean, explained the way you'd want it explained · Overreacted
- Summary: A hands-on tour of Lean's syntax, from def and #eval to proofs that run at typecheck time. Lean lets you write ordinary programs and then prove universal…
- Keywords: lean, functional programming, proofs, type systems, syntax, technology, design, explained, way, you'd, want, Overreacted
- Source: Overreacted — https://overreacted.io/a-lean-syntax-primer
- Read time: 4 min
- Topics: lean, functional programming, proofs, type systems, syntax, technology, design
## An opinionated first tour
Dan Abramov writes the Lean introduction he wishes he'd gotten. Incomplete by admission, possibly wrong in places, but shaped around what actually confused him.

> this is how I wish I was introduced to it, and what I wish was clarified
## Definitions use colon equals
Top-level values look like def name := "Alice" and def age := 42. The := matters: Lean reserves plain = for comparison, the way Go and Pascal do.

> Note you have to write := (assignment) rather than = .
## Types are there even unwritten
Hover over name and you get String. Hover over 42 and you get Nat, a natural number that starts at zero and climbs as high as you want. You can spell types out, or let inference do it.
## Nudging inference toward Int
Write -140 and Lean gives you an Int. Want 25 as an Int instead of a Nat? Annotate it as def roomTemperature : Int := 25, or wrap the expression as (25 : Int).
## Two ways to use Lean
You can run code, or prove facts about code, or do both in the same file. The primer starts with running, then turns to proving.

> One way to use Lean is to run your code. Another way to use Lean is to prove some facts about your code.
## Eval prints into your editor
Add #eval birthYear and the answer appears on hover and in the InfoView panel. Keep the InfoView open permanently, it is the main feedback loop.

> Lean InfoView is incredibly useful and I suggest to keep it open at all times.
## Main makes it a real program
Define main and run lean, run Scratch.lean to get output in the terminal. Compile to C instead and you can see the literal 1983 baked into the generated function.
## A theorem is a def with a goal
theorem my_theorem : age + birthYear = 2025 := by starts a claim. The declared type is the statement, and by drops you into tactic mode to build the proof interactively.

> A theorem is like a def, but aimed specifically at declaring proofs.
## Unfold until it's arithmetic
Each unfold swaps a name for its definition and the goal in the InfoView changes under you. 42 + birthYear, then 42 + (2025 - age), then 42 + (2025 - 42).

> It almost makes you feel like you're the computer, logically transforming the code towards the goal.
## Decide finishes the job
Once the goal is concrete arithmetic, the decide tactic closes it. No code ran. The fact was verified during typechecking, and simp [age, birthYear] does the unfolding for you in one line.
## Break the formula, break the proof
Change age to any other number and the proof still holds. Change birthYear to 2023 - age and it stops typechecking. The claim is load-bearing, not decorative.
## Namespaces open, sometimes locally
open IO lets you write println instead of IO.println for everything below that line. Add in to scope the shortcut to a single definition rather than the rest of the file.
## No parens, no commas
Function calls are f a b c, never f(a, b, c). This is the thing that trips up everyone arriving from JavaScript, and the article says to read it several times.

> I need to emphasize this. No commas and no parens are used for function calls!
## Parens are only for grouping
IO.println 2025 - age parses as (IO.println 2025) - age, and Lean fails hunting for subtraction between IO Unit and Nat. Wrapping (2025 - age) fixes it. Parens group, they don't call.

> something (f x y) a (g z)
## Let bindings, no return
Definitions can't nest, but let breaks a long expression into readable pieces inside one. The last line is the value, so there is no return statement anywhere.

> There is no need for a return statement here.
## A dozen ways to write one function
def birthYear currentYear := ..., the fully annotated version, and several fun forms all produce the same Nat → Nat. The concise form reads best unless you need an anonymous function.
## Add an argument, lose inference
Take age as a parameter and Lean gets stuck: it can't run typeclass search for subtraction when it doesn't know either type. The fix is to annotate, as in (currentYear age : Nat).

> typeclass instance is stuck
## Prove it for every input
Copy-pasting theorems for 42, 25 and 77 is just testing. Instead state a + birthYear cy a = cy for unknown cy and a. You get the types, never the values, because a proof covers all of them at once.

> it's a test for all possible inputs of that function that runs during typechecking
## Omega handles the unknowns
decide is a calculator and needs concrete numbers. omega checks equations containing variables, so unfold birthYear followed by omega closes the universal claim.
## For all, and what's implicit
∀ cy a moves the arguments inside the proof, introduced later with intro. Braces and brackets in signatures like IO.println's are arguments too, filled in by inference and by typeclass search.

> in Lean generics are just arguments (often implicit)
## Key takeaway

Lean lets you write ordinary programs and then prove universal facts about them, checked by the compiler instead of by test cases.