[Why3-club] (no subject)

Julia Lawall julia.lawall at lip6.fr
Wed Jan 30 13:36:19 CET 2019


I have the following orgnization of modules:

A parameterized by f

B uses A

C uses A and B and is parameterized by g

D uses A, B and C and provides a definition for f and for g
The definition for g relies on things defined in A and B.

How can I set this up?  In D, I cannot just clone C, because I can't make
the definition of g without having A and B.  If I clone B, then define g,
then clone C providing the definitions of both f and g, I get a type
mismatch related to a type defined in B.

Is there some way that I can parameterize C by B and then pass B in as a
parameter when I clone C?


More information about the Why3-club mailing list