> I consider even the second one to be mixing the proofs
> with the code, because there's no easy way that I can tell at
> a glance that `sortReallySorts' is a proof rather than a program.
But I consider that a feature and not a bug. :-)

    -- Lennart


Reply via email to