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: May 02 2025 at 03:31 UTC