Zulip Chat Archive

Stream: new members

Topic: prelude

Alex Zhang (Jun 18 2021 at 11:01):

What is the function of the command prelude. (I saw this as the first line of a file)

Kevin Buzzard (Jun 18 2021 at 11:04):

End users don't need to worry about this. This is all to do with core Lean files and development of stuff which is fundamental to the system. IIRC it means "this file is part of the stuff which is loaded initially by any Lean session, so in particular don't load it here" -- you might find that if you write prelude at the top of a file then you might not be able to do stuff like #print nat because not even that got loaded.

Last updated: Dec 20 2023 at 11:08 UTC