[Why3-club] inlining functions or explicit predicates

Claude Marché Claude.Marche at inria.fr
Tue Feb 19 15:50:25 CET 2019

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 at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club

More information about the Why3-club mailing list