Re: [isabelle] Collections: problems with sets of sets
I have been playing with the Collection framework lately and having
trouble when trying to set up executable sets of sets. The theory
below illustrates the problem: the function maxima is meant to
compute the maximal sets contained in a set of sets. Using the value
command, I can evaluate the function for the empty and for singleton
sets, but evaluation fails for any argument containing two or more
There seems to be a problem with the setup of type Dlist. I reduced your
example to a minimal one, which does not use the Collection framework.
The problem goes away when I remove the [code nbe] declaration that
comes after the instance proof of equal in Dlist.thy
I don't know about the precise semantics of [code nbe] wrt. normal code
equations, but it seems to override the previous code equation.
Maybe Florian can comment...
This archive was generated by a fusion of
Pipermail (Mailman edition) and