Stepeval is what Christopher pointed to in his first email, but he said it only works on a teeny weeny subset of Haskell.On Tue Jan 27 2015 at 8:26:55 AM Sumit Sahrawat, Maths & Computing, IIT (BHU) <sumit.sahrawat.apm13@iitbhu.ac.in> wrote:I found https://github.com/bmillwood/stepeval, which evaluates expressions step-by-step. It might be possible to modify it for equational reasoning.On 27 January 2015 at 04:17, Albert Y. C. Lai <trebla@vex.net> wrote:On 2015-01-18 06:46 PM, Christopher Done wrote:
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.
Is there any tooling anywhere out there that can take in a Haskell expression and reduce it by one step?
I suggest my friend Lev Naiman's proof assistant project "Netty"
https://bitbucket.org/naiman/nettyproject/overview
It is not specific to Haskell. It is a general-purpose calculational proof assistant.
If you want to take a look at a paper, it's somewhere on his home page:
http://www.cs.utoronto.ca/~naiman/ <http://www.cs.utoronto.ca/%7Enaiman/>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--_______________________________________________RegardsSumit Sahrawat
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe