Dear Claude, (* me again *) I did not notice the appset module.. oh so thanks, I’ll try to use it. But seems to be many sets:
Fset, appset, impset…. Thanks, -JJ- > Le 19 févr. 2019 à 15:50, Claude Marché <claude.mar...@inria.fr> a écrit : > > > Hello JJ, > > Short answer: with Why3 1.x you should use one of the modules appset.Appset > or impset.Impset to program with finite sets (depending on whether you want a > mutable data structure or not). More precisely you should clone one of these, > giving the value of type 'elt', in a very similar way as you would > instantiate the functor Set.Make in OCaml. > > Longer answer, of the previous mail too, should come soon... > > - Claude > > Le 19/02/2019 à 15:33, Jean-Jacques Levy a écrit : >> Dear Jean-Christophe + Friends, >> me again (* sorry *) .. a quick view about polymorphic equality: >> Equality in logic should be distinct from Equality in regular code, where >> the ghost attribute is prohibited. So if the problem with the ghost values >> is only about aggregated data with ghost components, we could still use >> ‘Fset’ functions in regular code on non ghost values… Correct ? Is this too >> simple minded ? >> Cheers, -JJ- >> _______________________________________________ >> Why3-club mailing list >> Why3-club@lists.gforge.inria.fr >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
