[Why3-club] inlining functions or explicit predicates

Claude Marché Claude.Marche at inria.fr
Tue Feb 19 16:45:55 CET 2019



Le 19/02/2019 à 16:02, Jean-Jacques Levy a écrit :
> 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….

See http://why3.lri.fr/stdlib/

set.Set: theory of mathematical sets

set.Fset: theory of finite mathematical sets

appset.AppSet: data structure for applicative finite sets, similar to 
OCaml's Set.Make

impset.ImpSet: data structure for mutable finite sets, that could be 
implemented in OCaml as ('a,unit) Hashtbl.t



More information about the Why3-club mailing list