Le 12/03/2018 à 16:23, Sandrine Blazy a écrit :
I have a function f : ‘a -> int. When I am defining
function sum_set (s: set ‘a) : int = sum s f
I got the following error message:
This term has type set 'a, but is expected to have type set1 ‘xi
What’s wrong with s in this definition ?
Given the error message, I would say that the "set" type used in "sum"
later got shadowed by another type with the same name.
Best regards,
Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
