4 ms·
This is not my area of expertise, but I clicked around those Agda bugs with some interest, and it seems like all those problems are stemming from the fact that
by Analemma_ 3y ago
This is not my area of expertise, but I clicked around those Agda bugs with some interest, and it seems like all those problems are stemming from the fact that they defined inf < inf. A couple people mentioned addressing the issue by getting rid of that, and others objected that it would cause more problems than it solved. What are those problems? Why is inf < inf?
- HappyPanacea 3y agoThis is also not my area of expertise, but considering they are using sized types to prove termination through well-foundness so they are probably suppose to be ordinals where we can have ω < ω+1 but for some reasons they decide to forgo to distinguish between everything larger than ω and denote it as inf. Edit: I found an explanation https://ionathan.ch/2021/08/04/sized-types.html https://ionathan.ch/2021/08/04/sized-types.html