Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes



> So if you just want the sum over the elements, how about using 
> list_size f xs - size xs?

That's a great idea. It may not be the most elegant solution, but it
sounds pretty foolproof. Thanks!




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