Re: [isabelle] primrec of datatype containing fset
> Special care is needed when recursing through permutative structures like sets and multisets. For example, the primrec version discussed here is _not_ equal to the 'fun' version of 'count', since it recursively collapses the numbers coming from subtrees that happen to have the same count. The 'fun' version is the correct one.
ah of course, you're right. Sorry for the mistake, Jeremy!
This archive was generated by a fusion of
Pipermail (Mailman edition) and