Disable importing prelude.

Stream: new members

[Alona]

Is there a way to not import Init.Prelude?

[Aaron Liu]

like this

prelude
-- you have now skipped importing `Init`
-- beware that some things might not work now

[Aaron Liu]

(the default is to import Init)

[Floris van Doorn]

Note: this is definitely not a recommended way of using Lean. Unless you know what you're doing, this is not what you want to do. There are e.g. no guarantees of consistency of Lean if you don't import (at least) some Init files.