Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide

2013-05-22 22:43 Tobias Nipkow:
> Most of the time, converting from sets to lists is a cloogy workaround because
> of problems defining some function directly on fnite sets.

Good point – that's what I tried first, but I couldn't figure out how to
make it work.

> I recommend to
> understand and use the appropriate fold combinator on lists instead.

You mean "on sets", right?

Here is what I tried unsuccessfully.  I posted in on stackoverflow, as
it's a proper question.



Christoph Lange, School of Computer Science, University of Birmingham, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
  Work-in-progress deadline 7 June;
→ OpenMath Workshop, 10 July, Bath, UK.
  Submission deadline 7 June;

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