Topic: issues with "import"
Sachin Gadgil (Mar 16 2021 at 06:27):
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
and it worked - it printed the factorial of 100 in lean.Infoview tab in vscode
However, when I tried following example
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
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