[Agda] nontermination and Sized types

[Manuel Bärenz]

On 05.10.20 09:14, Nils Anders Danielsson wrote:
> On 2020-10-03 09:33, vlad wrote:
>> IMO this bug and others (incompatibility of sized types with equality,
>> ...) should be better documented.
>
> It might be possible to fix the problems with sized types (see
> https://github.com/agda/agda/issues/2820), but I'm not aware of anyone
> that is working on that at the moment.
It would be great if someone could lead the development to fix these
issues at the upcoming Agda Implementors Meeting. I'd be interested to
participate but don't know where to begin.