Depend on Lean4 Library?

Stream: new members

[Ellis Kesterton]

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]

Don't you get that library for free?

[Ellis Kesterton]

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