Hello Sandrine,
> 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
Dear Ramana,
Indeed, this is apparently missing in lib/coq/set/Fset.v.
Here it is:
Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType
(fset a).
Proof.
intros.
split.
exists (fun _ => false).
exists nil. split; [ apply List.NoDup_nil | intuition; discriminate H ].
intros x y.
