Skip to main content
Proof Assistants Beta

Return to Question

added 49 characters in body
Source Link
Alex Byard
Alex Byard
  • 486
  • 1
  • 13

I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import packages?

Update: I've gotten git to work and I've managed to fork Mathlib. I used lake to set up a project, and now I'm having issues using import... anyone know how to help?

Update: I got it figured out. Should I share?

I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import packages?

Update: I've gotten git to work and I've managed to fork Mathlib. I used lake to set up a project, and now I'm having issues using import... anyone know how to help?

I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import packages?

Update: I've gotten git to work and I've managed to fork Mathlib. I used lake to set up a project, and now I'm having issues using import... anyone know how to help?

Update: I got it figured out. Should I share?

added 169 characters in body
Source Link
Alex Byard
Alex Byard
  • 486
  • 1
  • 13

I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import packages?

Update: I've gotten git to work and I've managed to fork Mathlib. I used lake to set up a project, and now I'm having issues using import... anyone know how to help?

I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import packages?

I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import packages?

Update: I've gotten git to work and I've managed to fork Mathlib. I used lake to set up a project, and now I'm having issues using import... anyone know how to help?

Source Link
Alex Byard
Alex Byard
  • 486
  • 1
  • 13

Lean 4 Importing into VSCode

I am working on Lean4 for a class project. I want to import some of mathlib4, but I keep getting "unknown package". I got Lean4 through the VSCode extension on Windows. How do I import packages?