[Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?

Jason Dagit dagit at codersbase.com
Mon Jun 7 22:26:09 EDT 2010

On Sat, Jun 5, 2010 at 8:10 PM, Thomas Hartman <tphyahoo at gmail.com> wrote:

> Here's two implementations of break, a snappy one from the prelude,
> and a slow stupid stateful one.
> They are quickchecked to be identical.
> Is there a way to prove they are identical mathematically? What are
> the techniques involved? Or to transform one to the other?

If you want a proof assistant, you could try using Haskabelle:

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100607/2b1c31d8/attachment.html

More information about the Haskell-Cafe mailing list