Dear Why3-club,
I'm working on a development that uses the Fset's module extensively and
would like to use Coq to prove a few goals. I notice there is no
WhyType instance for Fset.fset. While it is fairly straightforward to
derive one, it can get cumbersome to have to do so for each goal
Le 03/12/2020 à 09:24, Sandrine Blazy a écrit :
> My other question is about TryWhy3: which version of why3 does it use?
I am updating it at the time of release. So, it should be 1.3.3.
Best regards,
Guillaume
___
Why3-club mailing list
Hello,
I am using why3 version 1.3.3 and would like to add the Z3 and E provers to the
list of installed provers, so that they are triggered by proof strategies 0, 1
and more. I tried several versions (among those listed in
provers-detection-data.conf), including Z3 version 4.8.4 (that is
