Question about #REQUIRE

[fblanqui]

#REQUIRE does not seem necessary and can be ignored. What is it for?

[amelieled]

Same question for #NAME.

[francoisthire]

#NAME was deprecated, the time the libraries could be adapted.

#REQUIRE is not necessary but I know some situations where it is necessary.

Assume I have three modules (dk files):

The first one (X.dk)

def A : Type.

B : Type.

def a : A.

b : B.

The second one (Y.dk)

[] X.A --> X.B.

The third one (Z.dk)

[] X.a --> X.b.

The third one is not well-typed. However, if I add #REQUIRE Y. in Z.dk it becomes well-typed.

[francoisthire]

@fblanqui can this issue be closed? What do you expect to solve it otherwise?