モジュールパス解決とLean.findOLean

Leanサーバーは、環境変数LEAN_PATHなしでも、./lake-packages/some-package/build/lib/ の下を見ることは知っているようだ。import Foo は ./lake-packages/some-package/build/lib/Foo.olean をロードする。Lean.findOLean が役に立つ。

#eval Lean.findOLean `名前