Running Code from the terminal

Stream: new members

[David⚛️]

import Mathlib

def A : Fin 3 → Float := ![1.0, 2.0, 3.0]
def B : Fin 3 → Float := ![4.0, 5.0, 6.0]

def vectorAdd (A B : Fin 3 → Float) := A + B

-- Explicitly convert a vector (Fin 3 → ℝ) into a list of 3 elements
def vectorToList (v : Fin 3 → Float) : List Float := [v 0, v 1, v 2]

-- Main function to print the result of vector addition
def main : IO Unit :=
  IO.println s!"Vector addition: {vectorToList (vectorAdd A B)}"

Error on the terminal : unknown module prefix 'Mathlib
How do I fix this ?

[Bjørn Kjos-Hanssen]

I think this was discussed here:
https://leanprover.zulipchat.com/#narrow/stream/224796-Geographic-locality/topic/San.20Francisco.2C.20CA.2C.20USA/near/467328602

[Kevin Buzzard]

That code works fine for me. Looks like you're not running it in a project with mathlib as a dependency (or in mathlib itself)?

[David⚛️]

Kevin Buzzard said:

That code works fine for me. Looks like you're not running it in a project with mathlib as a dependency (or in mathlib itself)?

I just created another project with mathlib as a dependency and it's not working for me.

[Kevin Buzzard]

What's the error this time?

[David⚛️]

Kevin Buzzard said:

What's the error this time?

unknown declaration 'main'

[Derek Rhodes]

Hi @David⚛️, any luck? If you push your project to github, I'll clone it and try to get it working on my machine. Or maybe the issue will be more evident if people can see all the project files.