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
