# Zulip Chat Archive

## Stream: lean4

### Topic: issues with "import"

#### Sachin Gadgil (Mar 16 2021 at 06:27):

Hi All!

I have no experience with lean in general or lean4 in particular.

I installed lean4 on my machine (Ubuntu 20.04 with vscode as editor)

I wanted to start with some simple examples. 1st example I tried was

def fact x :=

match x with

| 0 => 1

| n+1 => (n+1) * fact n

#eval fact 100

from https://leanprover.github.io/lean4/doc/functions.html

and it worked - it printed the factorial of 100 in lean.Infoview tab in vscode

However, when I tried following example

import data.nat.basic

open nat

constant square : ℕ → ℕ

constant prime : ℕ → Prop

constant even : ℕ → Prop

variables w x y z : ℕ

#check even (x + y + z) ∧ prime ((x + 1) * y * y)

#check ¬ (square (x + y * z) = w) ∨ x + y < z

#check x < y ∧ even x ∧ even y → x + 1 < y

from https://leanprover.github.io/logic_and_proof/first_order_logic_in_lean.html

it shows error as "unknown package 'data'"

The code works, if use the 'try it' feature in the browser while accessing the webpage.

I see that no matter what package I try to import (while using vscode / lean4) it will give an error.

Not sure what is wrong - if the syntax has changed in lean4 or my lean4 install has any issues..

I tried searching for an answer but could not find it. Would appreciate your help!

#### Mario Carneiro (Mar 16 2021 at 06:29):

You probably want to be using lean 3. All the user documentation is targeting lean 3, and mathlib is on lean 3 (which is where data.nat.basic is coming from)

#### Mario Carneiro (Mar 16 2021 at 06:30):

Lean 4 is as yet only for the intrepid, it's not yet feature complete

#### Sachin Gadgil (Mar 16 2021 at 06:33):

Got it. Thanks for quick replay.

Let me know if there is any equivalent of "import" available in lean4 on experimental basis, or I just have to wait for it.

#### Mario Carneiro (Mar 16 2021 at 07:01):

There is the equivalent of `import`

, it's called `import`

. But there is currently no equivalent of `data.nat.basic`

, which is a file from mathlib, which has not yet been ported to lean 4

Last updated: May 18 2021 at 23:14 UTC