prelude

Stream: new members

[Alex Zhang]

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

[Kevin Buzzard]

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.