Module 1 · Level 1

Values & Basic Expressions

Lean starts with simple values: numbers, booleans, strings, and lists. You will use#eval to make sure every value has the type you expect.

Numbers and Booleans

lean

1#check 42        -- Nat
2#check (-3 : Int)
3#check true      -- Bool
4#check (3 < 10)  -- Prop

lean

1#check "Lean"            -- String
2#check [1, 2, 3]         -- List Nat
3#eval [1, 2, 3].length   -- 3

Exercise: Inspect Types

Create a small list of strings and ask Lean to tell you its type. Then use#eval to compute its length.

lean

1#check ["proof", "code", "types"]
2#eval ["proof", "code", "types"].length

ℹ

Prop is Lean's type of logical propositions. We will learn how proofs inhabit propositions later in the course.

Key Takeaway

Every value has a type. Lean will always tell you what it is if you ask.