Zulip Chat Archive

Stream: new members

Topic: Depend on Lean4 Library?

Ellis Kesterton (Aug 09 2023 at 10:15):

How do I depend on the Lean4 compiler library? The "lean4" repository on github does not seem to have a lakefile, so the usual method of "require _ from git _" does not seem to work

Eric Wieser (Aug 09 2023 at 10:24):

Don't you get that library for free?

Ellis Kesterton (Aug 09 2023 at 10:26):

Ah you're right whoops, I made a typo in the import path and assumed I needed to add it as a dependency

Last updated: Dec 20 2023 at 11:08 UTC