Stream: Coq users

Topic: Qualifying definitions by parent module


view this post on Zulip Théo Winterhalter (Nov 09 2020 at 09:50):

Hi. Let's say I have definitions split in several modules and I want to access them all using the same qualification, can I do it?
I can do

Require Export A B C.

in some module M so that Import M will put all the definitions of A, B and C at the top-level, but then A.foo can't be called M.foo. Is there a way to do that?

Thanks!

view this post on Zulip Gaëtan Gilbert (Nov 09 2020 at 09:52):

Include?

view this post on Zulip Théo Winterhalter (Nov 09 2020 at 09:59):

Ah yeah thanks, I had forgotten the name and was looking for Inline.
There is no one-liner right?

Require A B C.
Include A.
Include B.
Include C.

is the shortest I assume?


Last updated: Feb 04 2023 at 21:02 UTC