Meaning of "prelude" at start of lean 4 file.

Stream: new members

[Richard L Ford]

I'm reading the lean4 sources. Can someone tell me what is the effect of starting a file with "prelude"? I notice that Prelude.lean starts like that, so I thought it might trigger some kind of special treatment, but I see other files that start with "prelude" as well.

[Ruben Van de Velde]

The prelude is the code that's included when you don't import anything explicitly

[Anne Baanen]

(In Lean 3 at least) prelude means "don't import any files implicitly"

[Arthur Paulino]

I think it's the same in Lean 4:

prelude

#check Nat
-- unknown identifier 'Nat'
-- unknown constant 'sorryAx'

[Mario Carneiro]

Every file implicitly starts with import Init (lean 4) or import init (lean 3). Using prelude at the top of the file deletes this implicit import. This is required for any file that is imported by the Init module (i.e. the prelude itself) in order to avoid a circular import, but it is generally not recommended for anything else.

[Richard L Ford]

Thanks. That makes sense.