A benefit of pure functional programming is that it encourages equational reasoning.
However, the Haskell language has lacked direct tool support for such reasoning.
Consequently, reasoning about Haskell programs is either performed manually, or in
another language that does provide tool support (e.g. Agda or Coq).  HERMIT is a
Haskell-specific toolkit designed to support equational reasoning and user-guided
program transformation, and to do so as part of the GHC compilation pipeline.  This
paper describes HERMIT's recently developed support for equational reasoning, and
presents two case studies of HERMIT usage:  checking that type-class laws hold for
specific instance declarations, and mechanising textbook equational reasoning.