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: Aug 03 2023 at 10:10 UTC