Zulip Chat Archive
Stream: general
Topic: Prelude
Brandon Gomes (Jan 23 2020 at 22:20):
Is there any way to run Lean without the prelude loaded in?
Bryan Gin-ge Chen (Jan 23 2020 at 22:21):
Yes, put prelude at the beginning of your file.
Last updated: Dec 20 2023 at 11:08 UTC