Disable prelude?

Stream: lean4

[Siddharth Bhat]

I'm used to Haskell's {-# NoImplicitPrelude #-} to turn off all inbuilt/prelude declarations. Is there an equivalent in Lean?

[Chris B]

I think it's the same as it was in lean 3, you just put prelude at the top of the file.

prelude

/- unknown constant 'Nat' -/
#print Nat
/- unknown constant 'Eq' -/
#print Eq