leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: mathlib tutorial 5: invalid import: tuto_lib


Siyuan Yan (Nov 04 2022 at 06:54):

this line has an error:

▶ 4:1-4:2: error:
invalid import: tuto_lib
could not resolve import: tuto_lib

is it because of an updated mathlib? How should I fix it?
@Johan Commelin you might be interested?

Siyuan Yan (Nov 04 2022 at 06:57):

ohh, it's a local file in the solution directory but not in the exercise directory.


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll