In older versions of Why3 you probably needed to add `use import HighOrd`
- Claude
Le 07/05/2019 à 09:32, Guillaume Melquiond a écrit :
Le 07/05/2019 à 08:47, Aurélie Hurault a écrit :
Hello,
I'd like to use higher order functions in Why3, but I have trouble.
Which version of Why3 are you
Le 07/05/2019 à 08:47, Aurélie Hurault a écrit :
Hello,
I'd like to use higher order functions in Why3, but I have trouble.
Which version of Why3 are you using? I just tried with the latest
version (1.2.0) and your code works without modification (once [...] has
been replaced by three "use"
Hello,
I'd like to use higher order functions in Why3, but I have trouble.
Where, I try to write
module VerifStrat
[...]
constant n : int
function sum (f:'a -> int) (s: list 'a) : int =
match s with
| Nil -> 0
| Cons p q -> ((f p) + (sum f q))
end
lemma max : forall f : 'a ->
