标签
这篇博客文章详细描述了作者在Rocq中形式化《Dummit和Foote的Abstract Algebra》教材时发现的一个错误：关于单射函数和左逆的一个命题对空集不成立。
本文提出了一种从独立组件组合数据类型和函数的技术，并将该方法扩展到结合自由单子，从而实现了对Haskell的IO单子的模块化结构。