Email Gateway (Aug 18 2022 at 17:17): Email Gateway (Aug 18 2022 at 17:17):From: filip@matf.bg.ac.rs
Hello,
I have been successfully been using FSet theory included in development
releases for executable finite sets. In Isabelle2011 it has been renamed
to Cset.
Collecting all elements of a set of sets was possible in development
releases and the command
value "Supremum (Fset.Set [Fset.Set[1::nat, 2], Fset.Set[2, 3]])"
returned "Fset.Set [1, 2, 3]".
However, in Isabelle2011 the command
value "Supremum (Cset.set [Cset.set[1::nat, 2], Cset.set[2, 3]])"
fails with the message:
*** Wellsortedness error:
*** Type nat Cset.set not of sort complete_lattice
*** No type arity nat :: enum
although, there is
instantiation Cset.set :: (type) complete_lattice
which does not mention the class enum.
Any suggestions?
Best regards,
Filip
Last updated: Apr 19 2024 at 08:19 UTC