Regivan

Stream: new members

[Regivan Santiago]

Hello

[Kevin Buzzard]

You made it :-)

[Minchao Wu]

Hello

[Patrick Massot]

Welcome!

[Regivan Hugo Nunes Santiago]

Hello, I have installed lean and I want to import some theories. However VSCode states the following:

file 'Kenny_comm_alg/ideal_operations' not found in the LEAN_PATH

Could you help me?

[Kevin Buzzard]

Doesn't the error in VS Code point you to a web page which gives several suggestions about what to try next? This used to be the case

[Bryan Gin-ge Chen]

What steps did you take exactly? Kenny_comm_alg is presumably from some repo, did you get it using leanproject get name_of_repo?

[Jalex Stark]

You'll probably need to say a lot more before anyone can be helpful to you! As a quick sanity check, are you asking about taking lean 3 code and producing lean 4 code from it?

[Kevin Buzzard]

This question was also asked in another thread with no reference to lean 4 so I suspect it's a lean 3 question. What's more concerning is that Kenny_comm_alg isn't in mathlib either, it reminds me of an old attempt to define schemes

[Regivan Hugo Nunes Santiago]

Thank you for your comments. The following code has not problem in the web, however in my local installation I have problems:

import data.nat.basic
open nat

constant prime : ℕ → Prop
constant even : ℕ → Prop
constant odd : ℕ → Prop

#check ∀ x, (even x ∨ odd x) ∧ ¬ (even x ∧ odd x)
#check ∀ x, even x ↔ 2 ∣ x
#check ∀ x, even x → even (x^2)
#check ∀ x, even x ↔ odd (x + 1)
#check ∀ x, prime x ∧ x > 2 → odd x
#check ∀ x y z, x ∣ y → y ∣ z → x ∣ z

I take the message:

file 'data/nat/basic' not found in the LEAN_PATH

[Jalex Stark]

Do you have mathlib installed?

[Regivan Hugo Nunes Santiago]

Nope, how do I install it?

[Bryan Gin-ge Chen]

@Regivan Hugo Nunes Santiago these posts are a bit off topic for this thread which is about Lean 4 and mathlib. I'm going to move these posts to your other thread in the new-members stream. Please try to reply there if you can.

[Bryan Gin-ge Chen]

The recommended way to install Lean and mathlib is by following the directions appropriate to your OS on this page: https://leanprover-community.github.io/get_started.html