[Why3-club] (no subject)

François Bobot francois.bobot at cea.fr
Wed Jan 30 14:20:38 CET 2019

Le 30/01/2019 à 13:36, Julia Lawall a écrit :
> 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.

In a similar example, I was able to move the problematic type definition out of all these modules by
making it polymorphic.

Then you can more easily instantiate functions repeatedly in all the modules.

Does that work in your case?


More information about the Why3-club mailing list