[Why3-club] Finite vs infinite sets

Johannes Kanig kanig at adacore.com
Thu Nov 7 17:31:52 CET 2013

Hello Stefan,

On Thu, 07 Nov 2013 17:23:41 +0100, Stefan Berghofer <berghofe at in.tum.de> wrote:
> I would have expected this axiom to either have an additional assumption such as "finite s",
> or to use a different type such as "fset 'a" denoting finite sets. Maybe I am just missing something?

Yes, you probably missed the "clone" declaration at the beginning of theory FSet:

   clone export SetGen

A clone takes a theory and creates (different) copies of all symbols in it. If you add the "export" keyword, then the symbols of that clone become part of the theory you are currently in. So FSet.set is a different type than Set.set, just as you want it to be.



Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list