# QED Prover [![Hackage version](https://img.shields.io/hackage/v/qed.svg?label=Hackage)](https://hackage.haskell.org/package/qed) [![Build Status](https://img.shields.io/travis/ndmitchell/qed.svg)](https://travis-ci.org/ndmitchell/qed)

Experiments writing a proof system, particularly designed to prove properties about Haskell code, such as the [HLint rewrite rules](https://github.com/ndmitchell/hlint/blob/master/data/Default.hs).

Tom Ellis described the approach as "coinduction on the execution".