Formalisation of a proof of soundness of corecursive type-class resolution
This is a formalisation of a proof of soundness of corecursive type-class resolution as in Farka et al. [1]
The source code is documented in-line in comments, a highlighted version is provided.
Just @frantisekfarka for now.
[1] ...