[Why3-club] (no subject)
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