[Why3-club] (no subject)
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 attempted using Coq. Are there plans to add an instance in a future release? If not, how might I go about modifying my existing Why3 installation to include one? Thanks, Ramana Nagasamudram ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] provers triggered by proof strategies
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 Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] provers triggered by proof strategies
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 mentioned in the documentation for proof strategies). However, none of them is triggered by strategies 0 and 1. Which version of Z3 and E should I use? My other question is about TryWhy3: which version of why3 does it use ? Thanks, Sandrine___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
