Beginner, cannot import in Lean

Question

I am an absolute beginner, not a programmer, trying to learn formal verification with Logic and Proof. I cannot import anything in Lean.

I extract the tar file for the binary to /tmp then do

/tmp/lean-3.4.1-linux/bin/./lean /tmp/test.lean

It works except when I am importing anything. So if my file test.lean just says

open classical
example (P : Prop) : P ∨ ¬ P := em P

there is no error. But if the same file instead says

import data.set

I get the error message

/tmp/test.lean:1:0: error: file 'data/set' not found in the LEAN_PATH  
/tmp/test.lean:1:0: error: invalid import: data.set  
could not resolve import: data.set

A similar error occurs with import data.nat.

What am I doing wrong, and what should I do? I am using Ubuntu 16.04. Please note that since I am a beginner, I have never compiled anything from source.

Answer 1

These packages are hidden in init.

import init.classical
import init.data.nat
import init.data.set

But I believe that Lean imports everything in init by default, so you actually would not need the lines above.

You can also skip open and qualify invocations.

example (P : Prop) : P ∨ ¬ P := classical.em P