26 Jan
2015
26 Jan
'15
5:47 p.m.
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/