Hi 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 only know of stepeval: http://bm380.user.srcf.net/cgi-bin/stepeval.cgi?expr=foldr+%28%2B%29+0+%5B1%... But it's just a prototype and works on a teeny weeny subset of Haskell. As much as I like doing tooling, my bandwidth for this area is already full. It seems quite hard to implement such a tool with existing tooling. Real compilers and interpreters tend to be distinctly far away from a simple substitution model or retaining the original source code and being able to print valid source back out. If such a tool existed, though, it'd be super handy and you could probably include it as another check for your build process like your type checking, your quickcheck properties and your unit tests. I would personally invest a little bit of time to add interactive Emacs support for such a tool. Ciao