Zulip Chat Archive

Stream: lean4

Topic: issues with "import"


view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Mar 16 2021 at 06:30):

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

view this post on Zulip 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.

view this post on Zulip 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