[Agda] nontermination and Sized types

Nils Anders Danielsson nad at cse.gu.se
Tue Oct 6 12:16:57 CEST 2020


On 2020-10-03 15:24, James Wood wrote:
> My experience, as an occasional user of this stuff, is that `Size<` is
> broken, and you have to make do with `↑`, `_⊔_`, &c.

The problems are not restricted to Size<_:

   https://github.com/agda/agda/issues/2820#issuecomment-704172549

-- 
/NAD


More information about the Agda mailing list