qualified imports?

Stream: lean4

[Siddharth Bhat]

What is the equivalent of Haskell's import qualified fooin Lean? This controls the import so that any symbol defined in foo must be access as foo.member.

I'd like to import Random.lean and write a monad transformer for it that supplies randomness. I'd like to reuse the names randNat and randBool for their monadic variants. Therefore, I'd like to import Init.Data.Random qualified.

[Yury G. Kudryashov]

Not sure about Lean 4 but in Lean 3 namespaces and files are completely independent.

[Yury G. Kudryashov]

But you can hide your definitions into a namespace.

[Mac]

Siddharth Bhat said:

What is the equivalent of Haskell's import qualified fooin Lean? This controls the import so that any symbol defined in foo must be access as foo.member.

No such mechanism exists -- and might even require radical changes to the Lean core to support. You have to stick the object in a namespace at definition time if you want it to be conditionally openable / qualifiable.

[Mac]

I do wish such a feature did / could exist though...

[Siddharth Bhat]

Thank you for the explanation :)