There's a good screencast of this being done with Idris, which has tools like you mentioned for interactively solving proofs. In it, the author proves that an i

There's a good screencast of this being done with Idris, which has tools like you mentioned for interactively solving proofs. In it, the author proves that an instance of Monoid upholds its 'laws': properties like associativity that are only upheld by convention in Haskell. https://www.youtube.com/watch?v=P82dqVrS8ik https://www.youtube.com/watch?v=P82dqVrS8ik