<div dir="ltr">Stepeval is what Christopher pointed to in his first email, but he said it only works on a teeny weeny subset of Haskell. <br></div><br><div class="gmail_quote">On Tue Jan 27 2015 at 8:26:55 AM Sumit Sahrawat, Maths & Computing, IIT (BHU) <<a href="mailto:sumit.sahrawat.apm13@iitbhu.ac.in">sumit.sahrawat.apm13@iitbhu.ac.in</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I found <a href="https://github.com/bmillwood/stepeval" target="_blank">https://github.com/bmillwood/stepeval</a>, which evaluates expressions step-by-step. It might be possible to modify it for equational reasoning.</div><div class="gmail_extra"></div><div class="gmail_extra"><br><div class="gmail_quote">On 27 January 2015 at 04:17, Albert Y. C. Lai <span dir="ltr"><<a href="mailto:trebla@vex.net" target="_blank">trebla@vex.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 2015-01-18 06:46 PM, Christopher Done wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I quite enjoy doing equational reasoning to prove that my functions satisfy some laws, I like to type out each substitution step until I get back what I started with. The only trouble is that it's rather manual and possibly error prone.<br>
<br>
Is there any tooling anywhere out there that can take in a Haskell expression and reduce it by one step?<br>
</blockquote>
<br></span>
I suggest my friend Lev Naiman's proof assistant project "Netty"<br>
<a href="https://bitbucket.org/naiman/nettyproject/overview" target="_blank">https://bitbucket.org/naiman/<u></u>nettyproject/overview</a><br>
It is not specific to Haskell. It is a general-purpose calculational proof assistant.<br>
<br>
If you want to take a look at a paper, it's somewhere on his home page:<br>
<a href="http://www.cs.utoronto.ca/~naiman/" target="_blank">http://www.cs.utoronto.ca/~<u></u>naiman/</a> <<a href="http://www.cs.utoronto.ca/%7Enaiman/" target="_blank">http://www.cs.utoronto.ca/%<u></u>7Enaiman/</a>><div><div><br>
<br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div></div><div class="gmail_extra">-- <br><div><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Regards</div><div dir="ltr"><div><br></div><div>Sumit Sahrawat</div></div></div></div></div></div></div>
</div>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>