[plt-scheme] Is there a set data-type?

On Sat, Feb 06, 2010 at 03:46:13PM -0500, Todd O'Bryan wrote:
> On Fri, Feb 5, 2010 at 8:52 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
> >
> > 1. Sets and potentially infinite sets aren't esoteric. We need them everywhere.
> >
> > 2. For 10 elements? Use a list, Luke, use a list.
> >
> 
> 1. I did say *more* esoteric. :-) My senior project as an math
> undergrad was a recreation of the construction of the reals as Cauchy
> sequences of rationals, making sure that each step along the way was
> consistent with Zermelo-Frankel. I can't remember if I actually got
> around to proving that the reals were continuous before I ran out of
> time...

Was this machine-checked formalisation stuff?  Or just done to the same 
level of detail as the books on ZF itself?  The first time I heard of a 
project like this was Automath, which was based on type theory instead 
of ZF, but did manage to formalize Landau's Grundlagen.

-- hendrik