Re: [Why3-club] trying to use FsetSum.sum

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

[Why3-club] trying to use FsetSum.sum

Hi, I’d like to use the sum function of the set.FsetSum theory: function sum <> (set '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