Re: [isabelle] primrec of datatype containing fset



Hi Andrei,

> 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!

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.