A collection of proofs for some idris class instances. So far there are proofs for most or all Monoid instances, most or all Functor instances and some Applicative and Monad instances.
All modules listed in verified.ipkg should work. If a module is not listed then it either isn't compiling or I forgot to add it. In the latter case please send a pull request or make an issue.