fix imports #158
eric-wieserAnnotations
2 errors
|
Build project:
src/exercises_sources/friday/analysis.lean#L1
/home/runner/work/lftcm2020/lftcm2020/src/exercises_sources/friday/analysis.lean:1:0:
file 'measure_theory/measure/lebesgue' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
|
|
Build project
Process completed with exit code 1.
|