issues with "import"

Stream: lean4

[Sachin Gadgil]

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]

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]

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

[Sachin Gadgil]

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]

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