[Haskell-cafe] is there a way to prove the equivalence of these
two implementations of (Prelude) break function?
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...
More information about the Haskell-Cafe