Equational Reasoning Assistant (ERA)

ERA is a syntax manipulation tool that allows users to do equational reasoning on Haskell programs. It has a graphical interface, letting users point and click on expressions (or sub-expressions), and transform these expressions in well defined ways.

ERA comes with a large library of lemmas about Haskell prelude functions. When released, Era will also have a proof butler that will help with typesetting the proofs that the user has performed.