I think my only remark would be about the extensive use of \lambda where, which you have clearly been adopting now in favor of copattern matching. It is definitely shorter, but the copattern matching had the advantage that it displayed the judgmental equalities that hold by definition more clearly. Either way, I am happy to merge this PR as-is. Great job!
This is a very nice pull request!
I think my only remark would be about the extensive use of
\lambda where, which you have clearly been adopting now in favor of copattern matching. It is definitely shorter, but the copattern matching had the advantage that it displayed the judgmental equalities that hold by definition more clearly. Either way, I am happy to merge this PR as-is. Great job!