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

Attachment: 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

Reply via email to