Hi, I’d like to use the sum function of the set.FsetSum theory: function sum <> (set <http://why3.lri.fr/stdlib/set.html#set_8> 'a) ('a -> int) : int
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 ? Best, Sandrine
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
