Hi
Yeah, the precise details may vary, even :) But for teaching, an automatic tool that does graph reduction would be great. I don't mind if it's sloppy (directly apply definitions & pattern matching VS everything is a lambda abstraction) and only does simply typed lambda calculus (no type applications, no type classes).
Well come ON people, there's *got* to be enough big-wigs on this list to put *something* together! ;-)
It's been done, but never got to a released state: http://haskell.org/haskellwiki/Haskell_Equational_Reasoning_Assistant http://www.cs.york.ac.uk/fp/darcs/proof/ (screenshot: http://www-users.cs.york.ac.uk/~ndm/temp/proof.png) And neither of them will be of much use to a beginner. Haskell is too complex to reason about formally for a beginner, and reasoning "informally" isn't very easy to do - because its not a precise description of what to do. Thanks Neil