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

[Why3-club] CfP F-IDE: Formal Integrated Development Environment

== Call for Papers F-IDE 2018 4th Workshop on Formal Integrated Development Environment A satellite workshop of FLoC/FM2018 July 14, 2018 - Oxford, UK

Re: [Why3-club] some issues after a recent upgrade

Thanks Claude, You are correct the OSX temp directory as specified in the environment variable TMPDIR appears to be used. Neither the path nor the environment variable are in the .why3.conf directory. If why3 isn't directing this use, then it might be wp telling it to use this directory.

Re: [Why3-club] some issues after a recent upgrade

Le 09/03/2018 à 21:42, Goodloe, Alwyn E. (LARC-D320) a écrit : > warning: axiom c_euclidian does not contain any local abstract symbol The Frama-C developer team is aware of this issue: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2018-February/005401.html > Ambiguous path: > >