Proposal: Laws for mtl classes

Li-yao Xia lysxia at
Wed Apr 24 14:57:39 UTC 2019

On 4/23/19 3:15 AM, Andreas Abel wrote:
> Good initiative, Li-yao!
> To find out whether the laws are complete, I suggest to formalize the 
> theory of these monad in a theorem prover like Agda and prove the 
> completeness there.

Thanks Andreas. That's a good idea, I will work on a formalization!


More information about the Libraries mailing list