Zulip Chat Archive

Stream: lean4

Topic: qualified imports?


Siddharth Bhat (Oct 11 2021 at 00:36):

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 (Oct 11 2021 at 01:23):

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

Yury G. Kudryashov (Oct 11 2021 at 01:24):

But you can hide your definitions into a namespace.

Mac (Oct 11 2021 at 02:22):

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 (Oct 11 2021 at 02:24):

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

Siddharth Bhat (Oct 11 2021 at 09:41):

Thank you for the explanation :)


Last updated: Dec 20 2023 at 11:08 UTC