Recursively exporting symbols via require

[01mf02]

Writing require open <A> in a file B does not give access to definitions from file A in file C when C contains require open <B>. I would like some mechanism like Require Export in Coq, which allows precisely that. This will be useful when typechecking larger theories, e.g. from Isabelle.

[rlepigre]

I'm not particularly fond of that behavior in Coq, what is wrong with adding a require open <A> in file C?

[01mf02]

The problem is that e.g. Isabelle works by treating every imports like Coq's Require Export. That means that in any Isabelle theory T, we can access not only the symbols of all imported theories stated in T, but also the symbols of all transitively imported theories. To simulate this with the current (non-transitive) require open, this would amount to adding sometimes hundreds (if not thousands) of require open statements at the beginning of each file, to explicitly open all transitively required theories.

[fblanqui]

See remark by @amelieled (https://github.com/Deducteam/lambdapi/issues/705#issuecomment-857503964):

It's a bit strange, because if I understand correctly, you can write:

C.lp:

symbol c : TYPE;

B.lp:

require open tests.C;
symbol b1 : c;
symbol b2 : tests.C.c;

A.lp:

require open tests.B;

Then, you can use b1 or b2 on A.lp, but not their type.