Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)

Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or ...